
\chapter{Traversable functors\label{chap:9-Traversable-functors-and}}

\section{Slides}

\paragraph{Motivation for the \texttt{\textcolor{blue}{\footnotesize{}traverse}}
operation}

Consider data of type $\text{List}^{A}$ and processing $f:A\rightarrow\text{Future}^{B}$

Typically, we want to wait until the entire data set is processed

What we need is $\text{List}^{A}\rightarrow\left(A\rightarrow\text{Future}^{B}\right)\rightarrow\text{Future}^{\text{List}^{B}}$

Generalize: $L^{A}\rightarrow\left(A\rightarrow F^{B}\right)\rightarrow F^{L^{B}}$
for some type constructors $F$, $L$

This operation is called \texttt{\textcolor{blue}{\footnotesize{}traverse}} 

How to implement it: for example, a 3-element list is $A\times A\times A$

Consider $L^{A}\triangleq A\times A\times A$, apply $\text{map}\,f$
and get $F^{B}\times F^{B}\times F^{B}$

We will get $F^{L^{B}}\triangleq F^{B\times B\times B}$ if we can
apply \texttt{\textcolor{blue}{\footnotesize{}zip}} as $F^{B}\times F^{B}\rightarrow F^{B\times B}$

So we need to assume that $F$ is applicative

In Scala, we have \texttt{\textcolor{blue}{\footnotesize{}Future.traverse()}}
that assumes $L$ to be a sequence

This is the easy-to-remember example that fixes the requirements

Questions:

Which functors $L$ can have this operation?

Can we express \texttt{\textcolor{blue}{\footnotesize{}traverse}}
through a simpler operation?

What are the required laws for \texttt{\textcolor{blue}{\footnotesize{}traverse}}?

What about contrafunctors or profunctors?


\paragraph{Deriving the \texttt{\textcolor{blue}{\footnotesize{}sequence}} operation}

\vspace{-0.1cm}The type signature of \texttt{\textcolor{blue}{\footnotesize{}traverse}}
is a complicated \textsf{``}lifting\textsf{''}

A \textsf{``}lifting\textsf{''} is often equivalent to a simpler natural transformation

To derive it, ask: what is missing from \texttt{\textcolor{blue}{\footnotesize{}fmap}}
to do the job of \texttt{\textcolor{blue}{\footnotesize{}traverse}}?{\footnotesize{}
\[
\text{fmap}_{L}:(A\rightarrow F^{B})\rightarrow L^{A}\rightarrow L^{F^{B}}
\]
}{\footnotesize\par}

We need $F^{L^{B}}$, but the \texttt{\textcolor{blue}{\footnotesize{}traverse}}
operation gives us $L^{F^{B}}$ instead

What\textsf{'}s missing is a natural transformation \texttt{\textcolor{blue}{\footnotesize{}sequence}}
$:L^{F^{B}}\rightarrow F^{L^{B}}$ 

The functions \texttt{\textcolor{blue}{\footnotesize{}traverse}} and
\texttt{\textcolor{blue}{\footnotesize{}sequence}} are computationally
equivalent:{\footnotesize{}
\[
\text{trav}\,f^{\underline{A\rightarrow F^{B}}}=\text{fmap}_{L}\,f\bef\text{seq}
\]
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & L^{F^{B}}\ar[rd]\sp(0.45){\text{seq}}\\
L^{A}\ar[ru]\sp(0.45){\text{fmap}_{L}\,f^{\underline{A\rightarrow F^{B}}}}\ar[rr]\sb(0.45){\text{trav}\,f^{\underline{A\rightarrow F^{B}}}} &  & F^{L^{B}}
}
\]
}Here $F$ is an \emph{arbitrary} applicative functor

Keep in mind the example \texttt{\textcolor{blue}{\footnotesize{}Future.sequence}}
$:\text{List}^{\text{Future}^{X}}\rightarrow\text{Future}^{\text{List}^{X}}$

Examples: $L^{A}\triangleq A\times A\times A$; $L^{A}=\text{List}^{A}$;
finite trees 

Non-traversable: $L^{A}\triangleq R\rightarrow A$; lazy list (\textsf{``}infinite
product\textsf{''})

Note: We \emph{cannot have} the opposite transformation $F^{L^{B}}\rightarrow L^{F^{B}}$


\paragraph{Polynomial functors are traversable}

\vspace{-0.1cm}Generalize from the example $L^{A}\triangleq A\times A\times A$
to other polynomials

Polynomial functors have the form {\small{}
\[
L^{A}\triangleq Z\times A\times...\times A+Y\times A\times...\times A+...+Q\times A+P
\]
}{\small\par}

To implement {\small{}$\text{seq}:L^{F^{B}}\rightarrow F^{L^{B}}$},
consider monomial {\small{}$L^{A}\triangleq Z\times A\times...\times A$}{\small\par}

We have $L^{F^{B}}=Z\times F^{B}\times...\times F^{B}$; apply \texttt{\textcolor{blue}{\footnotesize{}zip}}
and get $Z\times F^{B\times...\times B}$ 

Lift $Z$ into the functor $F$ using $Z\rightarrow F^{A}\rightarrow F^{Z\times A}$
(or with $F.\text{pure}$)

The result is $F^{Z\times B\times...\times B}\triangleq F^{L^{B}}$

For a polynomial $L^{A}$, do this to each monomial, then lift to
$F^{L^{B}}$

Note that we could apply \texttt{\textcolor{blue}{\footnotesize{}zip}}
in various different orders

The traversal order is arbitrary, may be application-specific

Non-polynomial functors are not traversable (see \href{http://www.cs.ox.ac.uk/jeremy.gibbons/publications/uitbaf.pdf}{Bird et al., 2013})

Example: $L^{A}\triangleq E\rightarrow A$; $F^{A}\triangleq\bbnum 1+A$;
can't have {\small{}$\text{seq}:L^{F^{B}}\rightarrow F^{L^{B}}$}{\small\par}

All polynomial functors are traversable, and usually in several ways

It is still useful to have a type class for traversable functors


\paragraph{Motivation for the laws of the \texttt{\textcolor{blue}{\footnotesize{}traverse}}
operation}

\vspace{-0.2cm}The \href{https://arxiv.org/pdf/1202.2919.pdf}{\textquotedblleft law of traversals\textquotedblright\{\} paper}
(2012) argues that \texttt{\textcolor{blue}{\footnotesize{}traverse}}
should \textsf{``}visit each element\textsf{''} of the container $L^{A}$ exactly
once, and evaluate each corresponding \textsf{``}effect\textsf{''} $F^{B}$ exactly
once; then they formulate the laws

To derive the laws, use the \textsf{``}lifting\textsf{''} intuition for \texttt{\textcolor{blue}{\footnotesize{}traverse}},{\footnotesize{}
\[
\text{trav}:(A\rightarrow F^{B})\rightarrow L^{A}\rightarrow F^{L^{B}}
\]
}{\footnotesize\par}

{\footnotesize{}L}ook for \textsf{``}identity\textsf{''} and \textsf{``}composition\textsf{''} laws:

\textsf{``}Identity\textsf{''} as \texttt{\textcolor{blue}{\footnotesize{}pure}} $:A\rightarrow F^{A}$
must be lifted to \texttt{\textcolor{blue}{\footnotesize{}pure}} $:L^{A}\rightarrow F^{L^{A}}$

\textsf{``}Identity\textsf{''} as $\text{id}^{\underline{A\rightarrow A}}$ with $F^{A}\triangleq A$
(identity functor) lifted to $\text{id}^{\underline{L^{A}\rightarrow L^{A}}}$

\textsf{``}Compose\textsf{''} $f:A\rightarrow F^{B}$ and $g:B\rightarrow G^{C}$
to get $h:A\rightarrow F^{G^{C}}$, where $F$, $G$ are applicative;
a traversal with $h$ maps $L^{A}$ to $F^{G^{L^{C}}}$ and must be
equal to the composition of traversals with $f$ and then with $g^{F\uparrow}$

Questions:

Are the laws for the \texttt{\textcolor{blue}{\footnotesize{}sequence}}
operation simpler?

Are all these laws independent?

What functors $L$ satisfy these laws \emph{for all} applicative functors
$F$?


\paragraph{Formulation of the laws for \texttt{\textcolor{blue}{\footnotesize{}traverse}} }

\vspace{-0.15cm}Identity law: For any applicative functor $F$, 
\[
\text{trav}\left(\text{pure}\right)=\text{pure}
\]
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc}\ L^{A}\ar[rr]\sp(0.45){\text{pure}^{\underline{L^{A}\rightarrow F^{L^{A}}}}}\ar[rr]\sb(0.45){\text{trav}\,(\text{pure}^{\underline{A\rightarrow F^{A}}})} &  & F^{L^{A}}}
\]

Second identity law: $\text{trav}^{\text{Id}}(\text{id}^{A})=\text{id}^{L^{A}}$
is a consequence with $F=\text{Id}$

So, we need only one identity law

Composition law: For any $f^{\underline{A\rightarrow F^{B}}}$ and
$g^{\underline{B\rightarrow G^{C}}}$, \& applicative $F$ and $G$,
\[
\text{trav}\,f\bef\left(\text{trav}\,g\right)^{F\uparrow}=\text{trav}\,\big(f\bef g^{F\uparrow}\big)
\]
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & F^{L^{B}}\ar[rd]\sp(0.55){\ \ \ \ \text{fmap}_{F}\big(\text{trav}^{G}\,g\big)^{\underline{L^{B}\rightarrow G^{L^{C}}}}}\\
L^{A}\ar[ru]\sp(0.45){\text{trav}^{F}\,f^{\underline{A\rightarrow F^{B}}}}\ar[rr]\sb(0.45){\text{trav}^{F^{G}}\,h^{\underline{A\rightarrow F^{G^{C}}}}} &  & F^{G^{L^{C}}}
}
\]
where $h^{\underline{A\rightarrow F^{G^{C}}}}\triangleq f\bef g^{F\uparrow}$.
(Note: $H^{A}\triangleq F^{G^{A}}$ is applicative!)


\paragraph{Derivation of the laws for \texttt{\textcolor{blue}{\footnotesize{}sequence}} }

\vspace{-0.15cm}Express $\text{trav}\,f=f^{L\uparrow}\bef\text{seq}$
and substitute into the laws for $\text{trav}$:

Identity law:{\small{} $\text{trav}\left(\text{pure}\right)=\text{pure}^{L\uparrow}\bef\text{seq}=\text{pure}$}{\footnotesize{}
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & L^{F^{A}}\ar[rd]\sp(0.45){\text{seq}}\\
L^{A}\ar[rr]\sb(0.45){\text{pure}^{L^{A}}}\ar[ru]\sp(0.45){\text{fmap}_{L}\,\text{pure}^{A}} &  & F^{L^{A}}
}
\]
}{\footnotesize\par}

Naturality law: $\text{seq}\bef g^{F\uparrow L\uparrow}=g^{L\uparrow F\uparrow}\bef\text{seq}$
with $g^{\underline{A\rightarrow B}}$, mapping $L^{F^{A}}\rightarrow F^{L^{B}}$

Composition law: {\footnotesize{}
\begin{align*}
\text{trav}\,f\bef\left(\text{trav}\,g\right)^{F\uparrow} & =f^{L\uparrow}\bef\text{seq}\bef\left(g^{L\uparrow}\bef seq\right)^{F\uparrow}\\
 & =f^{L\uparrow}\bef\text{seq}\bef g^{L\uparrow F\uparrow}\bef\text{seq}^{F\uparrow}=f^{L\uparrow}\bef g^{F\uparrow L\uparrow}\bef\text{seq}\bef\text{seq}^{F\uparrow}\\
\text{trav}\,\big(f\bef g^{F\uparrow}\big) & =\big(f\bef g^{F\uparrow}\big)^{L\uparrow}\bef\text{seq}=f^{L\uparrow}\bef g^{F\uparrow L\uparrow}\bef\text{seq}
\end{align*}
}Now omit the common prefix $f^{...}\bef g^{...}$ and obtain: $\text{seq}\bef\text{seq}^{F\uparrow}=\text{seq}${\footnotesize{}
\[
\xymatrix{\xyScaleY{0.2pc}\xyScaleX{3pc} & F^{L^{G^{A}}}\ar[rd]\sp(0.6){\ (\text{seq}^{G})^{F\uparrow}}\\
L^{F^{G^{A}}}\ar[ru]\sp(0.45){\text{seq}^{F}}\ar[rr]\sb(0.45){\text{seq}^{F^{G^{?}}}} &  & F^{G^{L^{A}}}
}
\]
}{\footnotesize\par}


\paragraph{Constructions of traversable and bitraversable functors}

Constructions of traversable functors:

$L^{A}\triangleq Z$ (constant functor) and $L^{A}\triangleq A$ (identity
functor)

$L^{A}\triangleq G^{A}\times H^{A}$ for any traversable $G^{A}$
and $H^{A}$

$L^{A}\triangleq G^{A}+H^{A}$ for any traversable $G^{A}$ and $H^{A}$

$L^{A}\triangleq S^{A,L^{A}}$ (recursive) for a bitraversable bifunctor
$S^{A,B}$ 

If $L^{A}$ is infinite, laws will appear to hold but \texttt{\textcolor{blue}{\footnotesize{}seq}}
will not terminate

A bifunctor $S^{A,B}$ is \textbf{bitraversable} if \texttt{\textcolor{blue}{\footnotesize{}bisequence}}
exists such that
\[
\text{biseq}:S^{F^{A},F^{B}}\rightarrow F^{S^{A,B}}
\]
 for any applicative functor $F$; the analogous laws must hold

Constructions of bitraversable bifunctors:

$S^{A,B}\triangleq Z$, $S^{A,B}\triangleq A$, and $S^{A,B}=B$

$S^{A,B}\triangleq G^{A,B}\times H^{A,B}$ for any bitraversable $G$
and $H$

$S^{A,B}\triangleq G^{A,B}+H^{A,B}$ for any bitraversable $G$ and
$H$

All polynomial bifunctors are bitraversable

All polynomial functors, including recursive functors, are traversable


\paragraph{Foldable functors: traversing with respect to a monoid}

\vspace{-0.15cm}Take $F^{A}\triangleq Z$ where $Z$ is a monoid

The \texttt{\textcolor{blue}{\footnotesize{}zip}} operation is the
monoid operation $\oplus$

The type signature of \texttt{\textcolor{blue}{\footnotesize{}traverse}}
becomes $\left(A\rightarrow Z\right)\rightarrow L^{A}\rightarrow Z$

This method is called \texttt{\textcolor{blue}{\footnotesize{}foldMap}} 

The type signature of \texttt{\textcolor{blue}{\footnotesize{}seq}}
becomes $L^{Z}\rightarrow Z$

This is called \texttt{\textcolor{blue}{\footnotesize{}mconcat}} \textendash{}
combines all values in $L^{Z}$ with $Z$\textsf{'}s $\oplus$

It is convenient to define the \texttt{\textcolor{blue}{\footnotesize{}Foldable}}
type class

But it has no laws any more

All traversable functors are also foldable

The \texttt{\textcolor{blue}{\footnotesize{}foldLeft}} method can
be defined via \texttt{\textcolor{blue}{\footnotesize{}foldMap}} with
$Z\triangleq(B\rightarrow B)$:
\[
\text{foldl}:\left(A\rightarrow B\rightarrow B\right)\rightarrow L^{A}\rightarrow B\rightarrow B
\]


\paragraph{Traversable contrafunctors and profunctors are not useful}

Traversing profunctors with respect to functors $F$: effects of $F$
are ignored

All contrafunctors $C^{A}$ are traversable w.r.t.~applicative profunctors
$F^{A}$,{\footnotesize{}
\[
\text{seq}:C^{F^{A}}\rightarrow F^{C^{A}}\triangleq\text{pure}^{C\downarrow}\bef\text{pure}
\]
\[
\xymatrix{C^{F^{A}}\ar[r]\sp(0.5){\text{cmap}_{C}\text{pure}_{F}^{A}}\xyScaleY{0.2pc}\xyScaleX{3pc} & C^{A}\ar[r]\sp(0.5){\text{pure}_{F}^{C^{A}}} & F^{C^{A}}}
\]
}{\footnotesize\par}

But not profunctors that are neither functors not contrafunctors

Counterexample: $P^{A}\triangleq A\rightarrow A$; need $\text{seq}:\left(F^{A}\rightarrow F^{A}\right)\rightarrow F^{A\rightarrow A}$;
we can't get an $A\rightarrow A$, so the only implementation is to
return $\text{pure}_{F}\left(\text{id}\right)$, which ignores its
argument and so will fail the identity law 

Traversing profunctors $L$ with respect to profunctors $F$: effects
are ignored

Counterexample 1: contrafunctor $L^{A}\triangleq A\rightarrow R$
and contrafunctor $F^{A}\triangleq A\rightarrow S$, a \texttt{\textcolor{blue}{\footnotesize{}seq}}
of type $L^{F^{A}}\rightarrow F^{L^{A}}$ must return {*}{*}{*}

Counterexample 2: contrafunctor $F^{A}\triangleq\left(R\rightarrow A\right)\rightarrow S$
and functor $L^{A}\triangleq\bbnum 1+A$; \texttt{\textcolor{blue}{\footnotesize{}seq}}
must return $1+\bbnum 0$

So, the result is trivial and probably not useful

Laws of traversables allow ignoring the effects of $F$


\paragraph{Examples of usage}

Convert foldable data structures to list

Fold a tree to aggregate data

Decorate a tree with Depth-First traversal order labels

Implement \texttt{\textcolor{blue}{\footnotesize{}scanMap}} and \texttt{\textcolor{blue}{\footnotesize{}scanLeft}}
as \texttt{\textcolor{blue}{\footnotesize{}traverse}} with a state
monad

Traversal for a non-monadic \textsf{``}rigid\textsf{''} tree $T^{A}\triangleq A+T^{A\times A}$

The corresponding construction is $L^{A}\triangleq S^{A,L^{R^{A}}}$
where $R$ is applicative and traversable and $S$ is bitraversable

What \emph{cannot} be implemented as a traversal:

Breadth-first traversal for a tree as  \Tree[ [ 2 [ 3 4 ] ] 1 ]  

Depth labeling of a tree as  \Tree[ [ 2 [ 3 3 ] ] 1 ] {\footnotesize{} }{\footnotesize\par}


\paragraph{Naturality with respect to applicative functor as parameter}

The{\footnotesize{} }\texttt{\textcolor{blue}{\footnotesize{}traverse}}
method must be \textsf{``}generic in the functor $F$\textsf{''}:{\footnotesize{}
\[
\text{trav}^{F,A,B}:(A\rightarrow F^{B})\rightarrow L^{A}\rightarrow F^{L^{B}}
\]
}Which means: The code of \texttt{\textcolor{blue}{\footnotesize{}traverse}}
can only use \texttt{\textcolor{blue}{\footnotesize{}pure}} and \texttt{\textcolor{blue}{\footnotesize{}zip}}
from $F$

A functor {\footnotesize{}$F^{A}$ }is \textsf{``}generic in $A$\textsf{''}: have
{\footnotesize{}$\text{fmap}:\left(A\rightarrow B\right)\rightarrow F^{A}\rightarrow F^{B}$}{\footnotesize\par}

\textsf{``}Generic in $F$\textsf{''} means mapping {\footnotesize{}$\left(F\rightarrow G\right)\rightarrow\text{trav}^{F}\rightarrow\text{trav}^{G}$}
in some way

Mathematical formulation:

For any natural transformation $F^{A}\rightarrow G^{A}$ between applicative
functors $F$ and $G$ such that $F.\text{pure}$ and $F.\text{zip}$
are mapped into $G.\text{pure}$ and $G.\text{zip}$, the result of
transforming $\text{trav}^{F}$ is $\text{trav}^{G}$

Such a natural transformation is a morphism of applicative functors

Category theory can describe {\footnotesize{}$\left(F\rightarrow G\right)\rightarrow\text{trav}^{F}\rightarrow\text{trav}^{G}$}
as a \textsf{``}lifting\textsf{''}

Use a more general definition of category than what we had so far
(morphisms between type constructors)

\subsection{Monoid morphisms}

Given two monoid types $M$ and $N$, a function $\phi:M\rightarrow N$
is a \textbf{monoid morphism}\index{monoid morphism} if $\phi$ satisfies
the two laws:
\begin{align*}
{\color{greenunder}\text{identity law}:}\quad & \phi(e_{M})=e_{N}\quad,\\
{\color{greenunder}\text{composition law}:}\quad & \phi(p\oplus_{M}q)=\phi(p)\oplus_{N}\phi(q)\quad.
\end{align*}
These laws mean that $\phi$ translates the operations of $M$ into
the operations of $N$.

\subsection{Exercises}

\subsubsection{Exercise \label{subsec:Exercise-traversables}\ref{subsec:Exercise-traversables}\index{exercises}}

\subsubsection{Exercise \label{subsec:Exercise-traversables-1}\ref{subsec:Exercise-traversables-1}}

Show that any traversable functor $L$ admits a method 
\[
\text{consume}:(L^{A}\rightarrow B)\rightarrow L^{F^{A}}\rightarrow F^{B}
\]
for any applicative functor $F$. Show that traverse and consume are
equivalent.

\subsubsection{Exercise \label{subsec:Exercise-traversables-2}\ref{subsec:Exercise-traversables-2}}

Show that $\text{seq}:L^{F^{A}}\rightarrow F^{L^{A}}=\text{id}$ if
we choose $F^{A}\triangleq A$ as the identity functor. 

\subsubsection{Exercise \label{subsec:Exercise-traversables-3}\ref{subsec:Exercise-traversables-3}}

Show that the identity law is not satisfied by an implementation of
$\text{seq}:L^{F^{A}}\rightarrow F^{L^{A}}$ for $F^{A}\triangleq\bbnum 1+A$
when $\text{seq}$ always returns an empty option.

\subsubsection{Exercise \label{subsec:Exercise-traversables-5}\ref{subsec:Exercise-traversables-5}}

Show that $K^{A}\triangleq G^{H^{A}}$ is traversable if $G$ and
$H$ are traversable.

\subsubsection{Exercise \label{subsec:Exercise-traversables-4}\ref{subsec:Exercise-traversables-4}}

Show that all the bitraversable laws hold for the bifunctor $S^{A,B}\triangleq A\times B$.

\subsubsection{Exercise \label{subsec:Exercise-traversables-6}\ref{subsec:Exercise-traversables-6}}

For the tree-like type defined as $T^{A}\triangleq\bbnum 1+A\times T^{A}\times T^{A}$,
define a traversable instance. Verify that the laws hold, using a
suitable bifunctor $S^{X,Y}$.

\subsubsection{Exercise \label{subsec:Exercise-traversables-7}\ref{subsec:Exercise-traversables-7}}

For a tree type $T^{A}$ of your choice, implement a traversable instance
for right-to-left traversal order, and test that the tree is decorated
with labels as  \Tree[ [ 4 [ 3 2 ] ] 1 ]  

\subsubsection{Exercise \label{subsec:Exercise-traversables-8}\ref{subsec:Exercise-traversables-8}}

Implement a traversable instance for a \textsf{``}rose tree\textsf{''} $T^{A}\triangleq A+\text{List}^{T^{A}}$.
Represent $T^{A}$ via a suitable bifunctor $S^{X,Y}$ and show that
$S$ is bitraversable (use constructions).

\subsubsection{Exercise \label{subsec:Exercise-traversables-9}\ref{subsec:Exercise-traversables-9}}

Is the recursive type constructor $L^{A}\triangleq A+L^{\text{List}^{A}}$
traversable? Explain what sort of data container it is.

\subsubsection{Exercise \label{subsec:Exercise-traversables-10}\ref{subsec:Exercise-traversables-10}}

Given a monad $M$ and a monoid morphism $\phi^{:R\rightarrow S}$
between some monoid types $R$ and $S$, prove that $\phi^{\uparrow M}:M^{R}\rightarrow M^{S}$
is also a monoid morphism. (The types $M^{R}$ and $M^{S}$ are monoids
due to Exercise~\ref{subsec:Exercise-monad-of-monoid-is-monoid}).

\begin{comment}
Solution

The empty elements of the monoids $M^{R}$ and $M^{S}$ (by definition)
are $\text{pu}_{M}(e_{R})$ and $\text{pu}_{M}(e_{S})$ respectively.
The binary operations of $M^{R}$ and $M^{S}$ are
\begin{align*}
 & p\underset{M^{R}}{\oplus}q\triangleq p\triangleright\text{flm}_{M}\big(u^{:R}\rightarrow q\triangleright(v^{:R}\rightarrow u\oplus_{R}v)^{\uparrow M}\big)\quad,\\
 & p\underset{M^{S}}{\oplus}q\triangleq p\triangleright\text{flm}_{M}\big(u^{:S}\rightarrow q\triangleright(v^{:S}\rightarrow u\oplus_{S}v)^{\uparrow M}\big)\quad.
\end{align*}
To verify the properties of a monoid morphism, begin with the identity
law:
\begin{align*}
{\color{greenunder}\text{expect to equal }e_{M^{S}}:}\quad & \gunderline{e_{M^{R}}}\triangleright\phi^{\uparrow M}=e_{R}\triangleright\gunderline{\text{pu}_{M}\triangleright\phi^{\uparrow M}}=\gunderline{e_{R}\triangleright\phi}\triangleright\text{pu}_{M}=e_{S}\triangleright\text{pu}_{M}=e_{M^{S}}\quad.
\end{align*}
Now check the composition law: for any $p^{:M^{R}}$ and $q^{:M^{R}}$,
\begin{align*}
{\color{greenunder}\text{expect to equal }(p\underset{M^{R}}{\oplus}q)\triangleright\phi^{\uparrow M}:}\quad & (p\triangleright\phi^{\uparrow M})\underset{M^{S}}{\oplus}(q\triangleright\phi^{\uparrow M})\\
 & =(p\triangleright\gunderline{\phi^{\uparrow M})\triangleright\text{flm}_{M}}\big(u\rightarrow q\triangleright\phi^{\uparrow M}\triangleright(v\rightarrow u\oplus_{S}v)^{\uparrow M}\big)\\
{\color{greenunder}\text{naturality of }\text{flm}_{M}:}\quad & =p\triangleright\text{flm}_{M}\big(u\rightarrow q\triangleright(\gunderline{\phi\bef(}v\rightarrow\phi(u)\oplus_{S}v))^{\uparrow M}\big)\\
{\color{greenunder}\text{compute composition}:}\quad & =p\triangleright\text{flm}_{M}\big(u\rightarrow q\triangleright(v\rightarrow\gunderline{\phi(u)\oplus_{S}\phi(v)}))^{\uparrow M}\big)\\
{\color{greenunder}\text{composition law of }\phi:}\quad & =p\triangleright\text{flm}_{M}\big(u\rightarrow q\triangleright(v\rightarrow\phi(u\oplus_{R}v))^{\uparrow M}\big)\\
{\color{greenunder}\text{move }\phi^{\uparrow M}\text{ outside}:}\quad & =p\triangleright\text{flm}_{M}\big(u\rightarrow q\triangleright(v\rightarrow u\oplus_{R}v)^{\uparrow M}\bef\phi^{\uparrow M}\big)\\
{\color{greenunder}\text{naturality of }\text{flm}_{M}:}\quad & =\gunderline{p\triangleright\text{flm}_{M}\big(u\rightarrow q\triangleright(v\rightarrow u\oplus_{R}v)^{\uparrow M}\big)}\bef\phi^{\uparrow M}\\
 & =(p\underset{M^{R}}{\oplus}q)\triangleright\phi^{\uparrow M}\quad.
\end{align*}
\end{comment}


\subsubsection{Exercise \label{subsec:Exercise-traversables-10-1}\ref{subsec:Exercise-traversables-10-1}}

Given a monoid type $R$ and a monad morphism $\phi:M\leadsto N$
between some monads $M$ and $N$, prove that $\phi:M^{R}\rightarrow N^{R}$
is a monoid morphism between $M^{R}$ and $N^{R}$. (The types $M^{R}$
and $N^{R}$ are monoids due to Exercise~\ref{subsec:Exercise-monad-of-monoid-is-monoid}).

\begin{comment}
Solution

The empty elements of the monoids $M^{R}$ and $N^{R}$ (by definition)
are $\text{pu}_{M}(e_{R})$ and $\text{pu}_{N}(e_{R})$ respectively.
The binary operations of $M^{R}$ and $N^{R}$ are
\begin{align*}
 & p\underset{M^{R}}{\oplus}q\triangleq p\triangleright\text{flm}_{M}\big(u^{:R}\rightarrow q\triangleright(v^{:R}\rightarrow u\oplus_{R}v)^{\uparrow M}\big)\quad,\\
 & p\underset{N^{R}}{\oplus}q\triangleq p\triangleright\text{flm}_{N}\big(u^{:R}\rightarrow q\triangleright(v^{:R}\rightarrow u\oplus_{R}v)^{\uparrow N}\big)\quad.
\end{align*}
To verify the properties of a monoid morphism, begin with the identity
law:
\begin{align*}
{\color{greenunder}\text{expect to equal }e_{N^{R}}:}\quad & \gunderline{e_{M^{R}}}\triangleright\phi=\gunderline{e_{R}\triangleright\text{pu}_{M}}\triangleright\phi=e_{R}\triangleright\text{pu}_{N}=e_{N^{R}}\quad.
\end{align*}
Now check the composition law: for any $p^{:M^{R}}$ and $q^{:M^{R}}$,
\begin{align*}
{\color{greenunder}\text{expect to equal }(p\underset{M^{R}}{\oplus}q)\triangleright\phi:}\quad & (p\triangleright\phi)\underset{N^{R}}{\oplus}(q\triangleright\phi)=(p\triangleright\phi)\triangleright\text{flm}_{N}\big(u\rightarrow q\triangleright\gunderline{\phi\triangleright(v\rightarrow u\oplus_{R}v)^{\uparrow N}}\big)\\
{\color{greenunder}\text{naturality of }\phi:}\quad & =p\triangleright\gunderline{\phi\bef\big(u\rightarrow q\triangleright(v\rightarrow u\oplus_{R}v)^{\uparrow M}\bef\phi\big)^{\uparrow N}}\bef\text{ftn}_{N}\\
{\color{greenunder}\text{naturality of }\phi:}\quad & =p\triangleright\big(u\rightarrow q\triangleright(v\rightarrow u\oplus_{R}v)^{\uparrow M}\big)^{\uparrow M}\bef\gunderline{\phi\bef\phi^{\uparrow N}\bef\text{ftn}_{N}}\\
{\color{greenunder}\text{composition law of }\phi:}\quad & =p\triangleright\big(u\rightarrow q\triangleright(v\rightarrow u\oplus_{R}v)^{\uparrow M}\gunderline{\big)^{\uparrow M}\bef\text{ftn}_{M}}\bef\phi\\
{\color{greenunder}\text{definition of }\text{ftn}_{M}:}\quad & =p\triangleright\text{flm}_{M}\big(u\rightarrow q\triangleright(v\rightarrow u\oplus_{R}v)^{\uparrow M}\big)\bef\phi=(p\underset{M^{R}}{\oplus}q)\triangleright\phi\quad.
\end{align*}
\end{comment}


\section{Discussion}

\begin{comment}
this is chapter 9 of the functional programming tutorial traversable
functors to motivate the interrupted introduction of these factors
into practice I always remember the example that you have a list of
some data items and you want to process it by using a function like
this where you have a future as a as a result of this function and
the usual way of doing this in Scala is to use a function called future
dot sequence and I have seen this I have shown this in a previous
tutorial and the idea is that you want to process each element of
this list with this function and you have to wait until the entire
list is done so we have many separate computations for each element
of the list encapsulated by the future for each one of them you want
to wait until the entire list is done and basically this is the type
signature that you want in order to implement this computation you
have a list of a you have a function from a to future B and you want
to get a list of B as a result and you can get it in the future so
you have a future of lists of it as a result and that is the type
signature that the function future that sequence will allow you to
have with some work but in order to understand what this kind of computation
does we want to generalize from the future to an arbitrary type constructor
F and we want to understand what properties these type constructors
must answer so the list we have L and instead the future we have F
and the type signature of the function is like this so this function
is called Traverse I believe there\textsf{'}s also a future of traders with
a type signature like this that works on sequences we want to generalize
to some type constructors F and L and that\textsf{'}s what we will be able
to do once we understand the properties of this operation so this
operation can be implemented for instance if L is this type constructor
then what can we do in order to implement this operation well clearly
we have an LA and we can apply map F so f is this function we can
apply map F and the result will be this now in other words we have
not what we want probably wanders F lb Inc which would be this so
how can we get F of a triple from a triple of F\textsf{'}s or clearly we need
an operation that\textsf{'}s similar to zip zip would be FB times F be going
to F of B times B now we need to apply zip twice and then we get from
here to here so once we have the zip we will be able to implement
this traverse operation that\textsf{'}s the conclusion so far so it seems that
F needs to be a quick ative in order to be able to implement this
type signature for at least for this type constructor so for this
type constructor certainly it is easy to implement if F is if it has
a zip operation then we can implement it like this so that is going
to be a fundamental assumption not for the traverse operation to make
sense the type constructor F must be implicative now the type constructor
L on the other hand doesn't we don't know what that is it could be
applicative or not maybe we'll find out but for now let\textsf{'}s what say
L is traversable if it has this operation now in Scala we have a very
limited version of this Traverse which assumes L to be a sequence
so it\textsf{'}s not based on this idea of being traversable as such it\textsf{'}s just
that one of the properties of a sequence is that you can implement
this operation and we'll see why that is so but for me the example
with lists and futures or sequences of futures is the easy to remember
example that helps me remember the requirements for the traversal
duration so always think that I have a list of some items and the
processing makes me a future so L is a list F the future and then
it is clear that I want this kind of type signature I want to have
a single future and when that future completes I want to have the
entire list of process data that\textsf{'}s the easy to remember example so
not not the other way around for example not a list of future they're
not interested in having a list of futures I want a single future
with the final list of the results and so that\textsf{'}s why this example
helps me remember this somewhat complicated type signature where I
could easily make a mistake they will a to L of B today to have fun
being LF being instead of X well being it\textsf{'}s easy to mix them up but
so remembering this example that I'm starting with that what helps
me remember the time signature of triggers so the questions that I'm
going to answer in this tutorial in this chapter are to find out what
factors L can have this triggers operation to find out if we can simplify
with somewhat complicated type signature can we express it perhaps
through a simpler operation what are the laws that is reasonable to
require for this operation and finally to look at contractors and
pro fungus do they have also some kind of analog of this operation
in previous tutorials are started right away with practical examples
of usage in this chapter I will first do more theory to understand
in more detail and more deeply the properties of this operation that
will be easier to follow the usage examples so to simplify traverse
we notice that traverse is a kind of lifting of sorts it\textsf{'}s the arguments
can be permuted so these are two curried arguments so we can take
this one was the first argument and then we have la to FLV yes the
second argument so it\textsf{'}s a complicated kind of twisted lifting and
we have seen several times already that often you can find a simpler
natural transformation that is computationally equivalent to a lifting
so let\textsf{'}s derive that natural transformation that is equivalent to
traverse to derive it I asked the question so why can't we have F
map to do the work of Traverse f map would have this type signature
it Traverse sorry this is actually yeah so so this is the type signature
investment but Traverse needs F L be here instead of lfb so see this
F needs to be outside and that\textsf{'}s what\textsf{'}s missing so we need to transform
lfb with F inside into F L being with em outside so that\textsf{'}s the transformation
that is a natural transformation we expect to be equivalent the trailer
so what\textsf{'}s called a sequence so this is maybe not a very good name
sequence kind of suggesting that we change the or the order of L and
F in the functor composition not a very good name but that\textsf{'}s a traditional
name and I don't know how else to call it indeed we find that the
functions traversing sequence are computationally equivalent so this
is why well we have defined sequence likeness so then Traverse of
a function f is computed by first doing F map of F like we get here
then we get this and then apply this sequence function that I abbreviated
to seek which performs this lets transposition of the order the type
diagram looks like this so we start with a type LA and we can do Traverse
from it directly with this trap function which takes F and director
gives you from la f OB or you can first do F map so you have a function
f under L you get instead of la l FB and then you change the order
so you reorder the functions composition ever be to FM and the results
must be equal so for any value of this type you go up or horizontal
and the result must be the same value of this type that\textsf{'}s the definition
and as we have seen before this pattern implies that natural transformation
is defined as a composition of F map sub sorry and lifting is defined
as composition of F method natural transformation and then this natural
transformation is equal to lift and if you take identity instead of
F obviously and so then that\textsf{'}s a pattern we've seen time and again
where the result is that traversing sequence are computational global
you can derive one from the other and back and it gets the same function
back so I'm going to spend time through again since it\textsf{'}s exactly the
same proof as we had many times just a different type signature and
notice also F here is an arbitrary placated factor so these functions
don't use the structure of f other than that it is applicative so
that\textsf{'}s that\textsf{'}s an example we have seen just just before we implemented
a traverse function for this type constructor by applying the zip
function of F otherwise we don't you know what F is we just use zip
from it and so we are generic in the function in the functor F as
long as it\textsf{'}s implicit if we don't look at the structure of F we do
look at the structure of L so the Traverse function depends on the
structure of L but it doesn't depend on the structure of F it\textsf{'}s generic
images future that sequence has this type signature and that\textsf{'}s an
example of a sequence natural transformation you note we cannot have
the opposite transformation I'll show the example for that but well
for future analyst you could make an opposite transformation for a
future of a list and you produce a list or individual futures that
are going to be all already copies of this future mapped to select
one copy of the lid and of the element you can do that it\textsf{'}s kind of
useless to transform in the opposite way but what I will show on examples
is that it\textsf{'}s impossible to have this transformation in general and
arbitrary it\textsf{'}s possible for future not for arbitrary yeah so examples
of traversable function functors this example we have already seen
list is another example sequence in general and also finite trees
various shapes there and also traversable an example of an entre versatile
factor is there either Malad and also the lazy list or infinite product
or stream is sometimes called lazy string so let\textsf{'}s see why that is
so let\textsf{'}s implement the sequence for this type constructor first so
I'm going to define this file constructor for convenience and the
seek function is I'm just going to define directly it\textsf{'}s going to have
this type signature and that\textsf{'}s just a zip apply it twice and then
some reordering Oh nested tuple that results from the zip and we know
this is associative because we assume that F is applicative now I'm
using my own typeclass for F which I call the zip for applicative
but you can also use cats applicative just has a slightly different
name for things and it doesn't have the zip syntax so I like the use
of zip syntax so I'm using my own type process here but it\textsf{'}s equal
to standard implicit if that was so the sequence function has this
type signature just as we have seen in the case or filter balls lowlands
and applicatives it\textsf{'}s much easier to reason about this natural transformation
rather than the reason about the lifting it\textsf{'}s also will be the case
of laws or in simpler to formulate so that\textsf{'}s why I will always always
define just a sequence function I will not define a traverse function
the Traverse is easily defined in terms of a sequence - and I'm therefore
in this tutorial concentrating entirely on the sequence function I'll
never implement Traverse directly to save time so let\textsf{'}s have another
example that either as a functor either Z where Z is a constant type
then the sequence must have this type signature so it takes an either
of Z FFA and puts F outside so it\textsf{'}s pulls the function f from the
inside of our plan into the outside that\textsf{'}s the time signature of sequence
so how do we implement that all we need to match so if it\textsf{'}s the left
we have a Z to produce F of Z so the only way to do that is to use
the pure method okay I mean interchange there were there blinds here
the left z does not have any FFA and so in order to produce an F of
something we have to use the pure method from F and then we apply
that to the left of Z and then we get the right type if we have a
right of FA then all we need to do is to put the right inside the
width so we just map that we don't change the value of a we just wrap
it to wrap it into the right type construction so that\textsf{'}s the very
clearly simple implementation so if we actually write this type signature
using a shortcut notation then maybe it\textsf{'}s even easier to understand
how the sequence function works so if we have a Z then we just put
Z inside F using the pure if you cover away then we just put a 0 plus
a into that by mapping with the right type constructor so that we
don't change this value hey let\textsf{'}s see how to implement the sequence
method for the Fortran type so here\textsf{'}s a simple binary tree it has
a value of type a and belief and it has a branch of two trees so how
the hell does sequence work on a tree like we're in the leaf where
we just wrap in the leaf like we did with this either and if we're
in the branch then we apply the sequence method which is the same
sequence we're defining is a recursive function them so we recursively
apply the same since and as a sequence method to the left and to the
right branches of the tree and then we zip them together so then zip
is the operation in the F function wickety function so we can use
that zip them together we get an F of a pair two trees and then we
wrap that fear is a branch under the map so this map is under the
tree sorry under the F function so f is an arbitrary negative function
and we're using its methods map and zip here we used its metal period
but other than that we did not use any knowledge of F so it is in
this way that we are generic in the factor f we are not using any
knowledge about the structure of f other than it has that it has a
map and zip and puree method let us see examples of non traversable
functors so here\textsf{'}s an example it\textsf{'}s a reader mode with a parameter
in its non polynomial and so it will turn now that this is not reversible
so let\textsf{'}s see why what\textsf{'}s takes on applicative function f specifically
like option a and let\textsf{'}s find all implementations of this type signature
which is the pipe signature of sequence now all implementations turn
out to be just one and this implementation always returns none so
it always returns an empty option ignoring its argument so it is not
a very interesting implementation and we will see shortly that this
would not satisfy was overprotective of over a traversable contest
so this is this satisfies the pipe signature but it does not satisfy
the walls we haven't yet seen the laws but it is reasonable to say
that this function completely ignores its argument so it loses information
and typical walls for a lifting would be identity and Composition
laws identity law would tell you that some lifting is identity but
if it\textsf{'}s losing information it cannot be identity so it cannot preserve
the data that you give it but if people lose it will always return
empty option and so that\textsf{'}s reasonable to expect when this note is
not a good implementation and so there are no good implementations
- thank you let\textsf{'}s take another example and you'll see there\textsf{'}s there\textsf{'}s
one implementation for this so we can actually implement this type
signature for this duplicative functor this this code is what you
would expect it\textsf{'}s taking this function so what translate entire signature
let\textsf{'}s just e to the pair and this is pair of eternity doing now if
you have a eat to the pair and you can produce a pair of Italy in
d2 a that\textsf{'}s very easy just duplicate your your function so we do have
implementations from this book we're supposed to produce an implementation
of sequence as a generic in the function so we cannot look at the
structure from the functor F and have a different implementation for
every effort want to be generic and so because we can we cannot implement
it for some F we're stuck in this is not going to prevent reversible
functor let\textsf{'}s take another example where we have a pair so the pair
of some type and a polynomial function and let\textsf{'}s take this as the
implicated and again we find them there is an implementation so that\textsf{'}s
fine well this is actually traversable what\textsf{'}s considered the infinite
list so the infinite list class needs to be defined because we cannot
have the cursive type as a type an alien\textsf{'}s we have to have a class
and it\textsf{'}s a pair of value of type a underlays evaluated tail choosing
again an infinite list of time from all values of tightly so let\textsf{'}s
define a sequence method well we can actually define it it\textsf{'}s quite
easy you you take the head of the list you zip it with the recursive
implication of the same function sequence to the tail from the list
which will sequence were found commute the order of factories and
then you wrap it into the infinite list again so that\textsf{'}s similar to
what our implementation for the sequence operation on a tuple except
that it\textsf{'}s recursive and it turns out this is infinite recursion let\textsf{'}s
check that the even the simplest functor have the identity function
let\textsf{'}s define it like this put some type of class instances for identity
function ages tribunal was defined let\textsf{'}s define an example value of
an infinite list which is if you find like this it\textsf{'}s a recursive definition
we could do a lazy Val instead of def I believe but it\textsf{'}s just cleaning
doing them since it\textsf{'}s a recursive function and you see the tail of
the list will turn again the same list so it\textsf{'}s going to be an infinite
list of 123 on the whole the way to infinity so if we use sequence
on this value then we get a stack overflow interaction because it\textsf{'}s
an infinite recursion so it\textsf{'}s it\textsf{'}s an infinite loop there\textsf{'}s no way
to implement the Traverse of an infinite list because basically what
you would mean is we need to sequence like this we need to have a
list of F values so it\textsf{'}s an infinite list of an infinite list about
four days and that should be mapped into an f of infinite list of
is now how can we do that we need to pull F outside to the outside
of the title which means that we need to evaluate infinitely many
of these f\textsf{'}s in order to pull off outside mean generically that\textsf{'}s
what we need to do we need to evaluate infinitely many elements of
this infinite list in order to put F outside it\textsf{'}s impossible to just
pull F outside magically out of the infinitely many elements here
and so even when F is just an identity factor s won't work it\textsf{'}s impossible
to pull f outside I mean it would be possible for identity factor
of course but we have to be generic in the factor f we cannot use
any methods on F other than zip and map and so we don't know what
F is f could be something that needs to be evaluated in order to pull
a out of it and so because of that it forces us to evaluate infinitely
many elements before we even get a single value of this type and so
that will never end and so that\textsf{'}s impossible so for this reason an
infinite list is not reversible and finally I mentioned that the opposite
type signature isn't is unworkable so why let\textsf{'}s make an example calculation
so let\textsf{'}s say L is an easier which we know is reversible F is this
reader unit which we know is applicative so let\textsf{'}s find all implementations
of this time signature and we find they're not there is no implementation
of this type signature the reason is that this type signature would
have to map this function into this data but that is impossible you
cannot extract Z out of this so you could not possibly return the
Z because you need an integer so which integer are going to give imagine
that this integer is a different data type you don't you don't have
values of it necessarily for integer you could put 0 in that integer
sure but that would not be reasonable from other types so you cannot
possibly pull Z out of this because there aren't any special values
of this type and you can also not get this function because you only
have this function and this function could sometimes fail to return
an 8 could sometimes return a Z so for some integers it could return
is e and you don't know in advance for which integers it will return
Z and for which it will return in a until you run this function on
every possible integer you won't know that and so that\textsf{'}s impossible
to know and so you can't split this into a Z and into it you couldn't
either split it into two functions into Z and into in the same for
the same reason you in order to split it you'd have to run this function
on every possible integer and see what the results are so that\textsf{'}s unworkable
and so that\textsf{'}s why you don't have that\textsf{'}s that\textsf{'}s an informal reason
why you don't have any implementations of this type and a final comment
is that there are several ways of implementing the sequence usually
so let\textsf{'}s consider this type again we have seen we can implement a
sequence by applying zip to x and here\textsf{'}s another implementation we
can arbitrarily select a different order so we instead of zipping
one two three with zip to one I'm sorry this is a mistake two three
say 1 and that\textsf{'}s valid so the type is right and the laws will hold
as well we'll see why so that shows you that there\textsf{'}s more than one
way of implementing the Traverse or in the sequence function which
is equivalent for a given type constructor L different valid ways
of doing it so let\textsf{'}s find out if other polynomial factors are traversable
now one of the central results here is that all polynomial functions
are reversible we will show this quite rigorously later so for now
let\textsf{'}s see how we can implement the Traverse or the sequence function
for an arbitrary polynomial function so we have done it so far for
this and we have also done it for either which is a simple polynomial
factor and the general polynomial factor would have this form it\textsf{'}s
got a polynomial in a with some constant coefficients which I here
denoted as Z Y Q P so we have seen how to implement for a monomial
so let\textsf{'}s first consider monomial like this so one part of this polynomial
then we can apply zip to these so first we look at lfb so RV has this
type so we can apply zip to these we get this and then we can lift
the Z into the functor F by just this standard factor map this function
is always possible for any factor f alternatively we can do F pure
of this Z and then this will become FZ and then we can zip it together
with all others but the result will be exactly the same as using this
function because of the law of identity for applicatives so the result
is going to be this and then that\textsf{'}s a sequence method for a single
monomial and then for each normal you do this and you have a disjunction
of different results of type F of a monomial and then we lift it to
F of the disjunction like we did in the either implementation so we
we have seen therefore that we can perform the traversal equivalently
the sequence operation on monomials and we can also perform them on
disjunctions and therefore we can perform them on arbitrary disjunctions
on monomials and that\textsf{'}s arbitrary polynomial factor also note we could
apply zip here in different orders wicked first zipless and then Z
put Z on the right we can change orders in different ways and so traversal
order could be application-specific it could be necessary to adjust
it for a certain application you can always implement in some order
or automatically say but it might not be necessarily correct for your
application and also we have seen that non polynomial factors at least
some of them are not to her so so this is not reversible because we
cannot have a reasonable implementation of this that does not lose
information and there\textsf{'}s this paper that I'm referencing here it\textsf{'}s
a complicated paper there in theoretical but it has a proof that only
polynomial functions are reversible that that and and also they must
be finite so infinite lists do not fit the conditions of their theorem
only finite containers polynomial factors are essentially containers
with data they can have different shape they can have many items of
data or few or none it could be a disjunction of different shapes
and they also can have extra data of some constant type in addition
to data of the type a but those are the containers that are traversable
and no other containers aren't reversible sorry you have a lazy infinite
stream that\textsf{'}s not reversible they have to be finite and they have
to be polynomial so that is proved in this paper in a complicated
way so I'm not going to try to understand how they did it I believe
that this is so because I have examples that even the simplest non
polynomial factor can't have reasonable implementation of sequence
so even though all polynomial functions are traversable they are usually
traversable in several different ways and so it\textsf{'}s useful to have a
typeclass to declare a specific instance of a typeclass expressing
a specific order of traversal so this order of zipping that we can
choose here corresponds to ordering of traversal in a sense we'll
see that when we look at specific examples of traversing but now let\textsf{'}s
take a look at the laws because we have have been talking about the
laws so far and we need to see more in more detail how they work so
I prefer to look at this type signature of Traverse and to derive
laws using the lifting intuition so it\textsf{'}s a lifting of sorts and every
time we had lifting so far we had laws of identity and Composition
in other words there was some kind of identity here and some kind
of composition of these and this has to translate into identity here
and composition of these I will mention that there is this paper which
is arguing what laws traversals must have from a different perspective
not as formally as I have argued just now because my argument is completely
formal Traverse looks like a lifting therefore it should have laws
like the laws we had before for other liftings it\textsf{'}s purely a formal
argument saying that the form of this function is similar therefore
it should have similar laws but this argument doesn't look at what
Traverse actually does well what it does is that it evaluates some
function on each element this one produces some effect maybe this
F is an applicative factor which could be a monad or it could be known
more and what it encapsulate some kind of effect some kind of computational
context or a result other than B and all these contexts need to be
somehow put together and be outside of the elbe so we need to reconstruct
our container L inside the larger effect described by F so we need
to somehow combine all these effects for individual values of a into
one big effect which will be outside and then we have to combine all
the values of B after somehow pull them out combine them again into
the same shape as the container L inside the F so all that needs to
be done by the traversal function and the authors of that paper argued
that the traversal first of all should visit each element of the container
exactly once it it should evaluate each effect exactly once and then
combine these effects into a larger effect and using this intuition
they formulate some laws that seem to fit this description in some
way well they didn't actually derive these laws from these requirements
but they showed examples where these requirements are violated and
they showed that these examples also violate the laws so this is a
little not very convincing to me that these laws are correct and therefore
I prefer the more formal approach because I have more assurance but
if I find some reasonable identity and Composition laws that\textsf{'}s a correct
set of laws so far in every example we have seen with functors with
contra factors filterable applicative and wounded every single example
had a function with type signature like this which was life like a
lifting in my terminology and in every single example there were identity
law and composition law and these laws were equivalent to all the
other set of laws that were derived from intuition and these laws
also corresponded to some category laws now in this example I don't
know how to formulate this in terms of a category and everything a
way that would be simple enough so I'm satisfied that I find a law
that looks like identity law and the law that looks like a composition
law even though I'm not satisfied that I can find it easy enough category
to reason about so that it\textsf{'}s useful so I'm not going to talk about
the category in this chapter I'm not going to describe this as a lifting
from one category to another because I don't know if that\textsf{'}s really
very useful and I don't know a good formulation of that so let\textsf{'}s look
for these laws so identity law is that we map some special function
here that is identity in some sense into a function here that plays
the role of identity now the type signatures are not a to a they are
a to f of B so what could be playing the role of identity here well
the pure method obviously and F has that method by an assumption so
the identity law is that if we put a pure method here than it should
be lifted to this which is again a pyramid and except it\textsf{'}s applied
to a different type of parameter now another way of formulating identity
is to say that if F is the identity function so then there\textsf{'}s no F
you just be then identity function here is all ordinary a to a and
that should be lifted to identity elite really so f is just identity
function and then this identity should be lifted to this so that is
another way of formulating an identity law let\textsf{'}s find out now to compose
what will be the composition if we have two of these functions like
f and G then we can compose them using F map but the result would
be this because the F G would be nested now we take F be we map G
over it and we get F of G of C now if F and G are in clique are applicative
then the composition F of G is also applicative we know that from
the properties of the platitudes and so it is again a function of
the same type except that it has a different factor instead of F so
f function G factor and the composition of such functions is going
to be of this kind which which is kind of complicated it changes the
functor each time so what should be on the right-hand side what should
be a composition of these traversals now the composition of traversals
obviously works in the same way so you have la 2 FL b and then FL
b 2 f g LC and so that is your final traversal and that should be
equal to applying the traversal right away with this function as a
purgative factor so in other words applying traversal to this if that
is true then traversal of composition is equal to composition of traversals
so that\textsf{'}s with a little twisting where we keep using F map in order
to get composition and keep pulling all the functors F and G all the
implicit is we keep pulling them outside with these twists it looks
like just a composition law traversal of composition of F and G with
some twisting is equal to the composition of the two traversals with
F and with G again with some twisting so these are the laws we're
going to examine and it will turn out these are exactly the same laws
as this paper proposes when I first looked at this it looks like we
have two identity laws are they really independent no they are it
will see that but that\textsf{'}s a question we need to answer also laws for
sequence are probably going to be simpler because in our experience
so far always we found that the laws became simpler if we consider
the natural transformation instead of a lifting so let\textsf{'}s find those
laws for the sequence and finally with the laws in in hand we can
try to answer the question of which functors satisfy these laws we
have found examples where we can implement the type signatures but
are the law is respected by those examples or not so that\textsf{'}s the questions
that we have after this point so let\textsf{'}s look at the first item the
dual so a traverse of pure needs to be Pierce and how fast if it\textsf{'}s
the first law let\textsf{'}s look at the type diagram for this so we started
from away we map it with pure where we map it with traverse of pure
and it should be the same value it was type in favilla so that\textsf{'}s the
first one now the second identity law looks like this and it\textsf{'}s clearly
a consequence of the first identity law if we just put F to be the
identity founder and the first law should hold for every applicative
functors so we really just need this one law when the second one is
a consequence so let\textsf{'}s forget it so we have the identity law which
is this and we have the composition law which we can write like this
and the short notation so for any function of this type and the function
G of this type and for any applicative factors F and G we have so
the composition of F and G is twisted in the sense that G must be
lifted by factor F so this is our twist on the composition other than
that composition of two traversals is equal to Traverse of composition
here will we twist and here we twist let\textsf{'}s look at the type diagram
we start again with LA first with Traverse with function f and we
get F lb well then we want to traverse with G but G works on B so
we have to we have to traverse just on this lb and F needs to stay
outside therefore we use F map of F and we Traverse inside of F using
the Traverse of G which is giving us this value F G LC or we could
directly Traverse on the function H with respect to the factor f of
G which is a functor composition so the factor H could be defined
like this as a functor composition of F and G and we know it\textsf{'}s applicative
so we could just directly Traverse with respect to H so this can be
traversal with respective H of a function H of this type this function
is defined like that so this is the law that we demand now which will
hold let\textsf{'}s derive the corresponding law for laws for its sequence
to do that we just Express Traverse like this your sequence and substitute
that into the laws of chillers so let\textsf{'}s look at identity law Traverse
of pure equals P R so Traverse of pure equals this conduction legal
pure so that\textsf{'}s the law of identity for pure so pure lifted to Bill
and then sequence should be the same as pure applied to the type parameter
Helle I should also mention naturality law that\textsf{'}s always the case
for all of our examples so far such as filterable moon and imitative
but all these natural transformations as well as the liftings they
have natural tea laws for each type parameter that they have there\textsf{'}s
one neutrality law which expresses the fact that the code implementing
that function does not use any information about the type it\textsf{'}s completely
generic in that type and so you can map this type to another type
before the transformation or after the transformation and the results
are going to be the same so here\textsf{'}s what the naturality law looks like
for the sequence now sequence has a more complicated type signature
and its type parameter a is all the way inside therefore in order
to transform in this a to some B we need to have a double F map so
let\textsf{'}s say there\textsf{'}s some function G that transforms a to be in order
to transform this a or transform that a we need to lift this G twice
and that\textsf{'}s how I would write it down so first we can sequence this
LF a to FL a and then we can lift G twice in this order or we can
first lift G twice in this order so that instead of LF a we get LF
B and then we sequence on that so that should be the same function
that\textsf{'}s a natural t law and the code for sequence will automatically
respect that law if it is a code that is generic type parameter a
will never use any information about the type of a so usually naturality
laws are satisfied automatically by generic code and so it\textsf{'}s not important
to check them but it\textsf{'}s important to check the other laws so now let\textsf{'}s
look at the composition law we need a bit more work about it traversal
of F followed by the traversal of G lifted so let\textsf{'}s substitute the
definition of traversal and then we get this formula now we can decompose
a lifting of composition going to factor law so we can get like this
now naturality law means we can interchange this and we get that and
finally the right hand side is written like that so again we can do
that because of the thumb tree law so in other words the composition
law for traverse says that this is equal to this they have a common
prefix that we can omit because these are arbitrary functions F and
G for which this must hold and so it\textsf{'}s sufficient that these things
are equal so that\textsf{'}s the law for sequence much simpler and here\textsf{'}s the
type diagram because the type types here are actually complicated
so we start with an L of F G C C is some type parameter I could use
a here but I just can't see now first we sequence with with respect
to F and then we just pull F out and we get F LGC then we sequence
with respect to G but we lift it to be operating inside of F so that
means we interchange this L and this G the result is f G LLC alternatively
we could sequence with respect to the factor f of G this is maybe
not a very nice known notation not very consistent but this is the
composition of functions F and G so it\textsf{'}s the page I mentioned here
I should probably for clarity I should use page instead of F G and
so if we sequence with respect to F G that means we pull out F G at
the same time to the outside and we get F G of LC so the result of
these two computations must be the same having formulated the laws
now can look at constructions and we can check that the laws hold
we can also check whether some factors can be traversable when they
are polynomial or when they recursive or they're not polynomial so
we have so far seen some examples but now let\textsf{'}s be more systematic
about it here are the constructions that I found for traversable factors
and I will go through each of them one by one now now before I do
that let me explain what is a by traversable and by functor so by
factor is a type constructor with two type parameters which is a functor
in both of them so it has a map with respect to each of them separately
and it also has a map with respect to both of them at once of course
because you can just you can transform a to some C and B to some D
separately or at the same time if you wish it doesn't doesn't it so
that\textsf{'}s a bi functor and by factors are by traversable in the following
sense they have this natural transformation where we have an F wrapping
each of the type parameters of s and this F can be pulled out by this
sequence by sequence natural transformation and it should be natural
both an A and B separately so that\textsf{'}s the assumption and so you see
this a and B remains and we have pulled F out to the outside so if
statute transformation exists which is natural in both a and B and
it has the same laws the laws of identity and the laws of composition
now the law of identity is this and it needs to be adapted obviously
to this by seek so that you have pure here and pure here and the law
of composition obviously needs to be adapted as well because we have
F G a F G B and so on but other than that it\textsf{'}s a direct generalization
so analogous laws must hold so let me now begin by deriving the laws
that must hold for these constructions rather deriving the fact that
the laws hold for these constructions first construction is constant
functor and identity factor so both of them are traversable till you
find that we need to define the sequence method and to show that the
laws hold for it that\textsf{'}s very simple so for convenience I'm just going
to put a type parameter up front the constant factor is a function
that doesn't end on its type parameter so L of F of a is the same
as I've elevated Simon is this constant times e and FMLA is f of Z
so sequence is this type signature and clearly this is f dot P R is
just a pure of F functor can't in any other way produce a type signature
like this but is generic in if we're not allowed to know what F is
except that it has a pyramid zip and map so let\textsf{'}s just define that
as a pure let\textsf{'}s check Louis so the identity law is that F map of pure
followed by sequence must be equal to F dot P R now I'm putting here
this underscore ell notation for clarity I could have said for example
instead of F dot P R I could have said pure underscore F what I mean
by this is that it\textsf{'}s the method that is defined for the type instructor
F such this method is not generic and F it is defined for each F separately
in the typeclass instance similarly F map is not generic and L it\textsf{'}s
defined for each L separately so I could I could have written like
this as well it\textsf{'}s not Scala notation necessarily but it will do for
now just for clarity to remind myself where these methods come from
now sequence is defined for L so here I could write it like this to
remind myself that the sequence is defined separately for each ill
but it is generic and F so I could write it like that so sequence
has F as a type parameter but L as type constructor or or functor
for which it is defined in the Thai class now so let\textsf{'}s see if we can
verify this law F map is identity for the constant factor so this
is identity and so this is just F here sequence is sorry F map of
F of F here is identity function f map does not transform anything
because there is nothing to transform we only have this Z cannot transform
so this is just at the energy function you can cross it out and then
we have the law that sequence equals pure at sequence equals pure
by definition so the law is satisfied let\textsf{'}s consider now the composition
law which is the composition of sequence of F and the lifted sequence
of G so now I'm using this notation with more sense in here I didn't
have to say it\textsf{'}s sequence Hamilton if I could just say sequence but
here it is important now to say which for which type parameter is
because the factor is a type parameter in sequence function so we
have the sequence applied with respect to applicative factor f and
this with respect to G and F G is the factor which is the composition
of F and G we just {[}Music{]} denote it like that for gravity so
this is now sequence is defined as pure F map is {[}Music{]} defined
in with respect to F so this is f naught F naught F naught L F map
l was identity but F map F is not and we actually don't know what
it does because it f is an arbitrary let\textsf{'}s look at your family so
you need to keep it symbolic so we have f dot P R which is this sequence
and then because the Scala operation and then responds to my composition
symbol and then we have F map F of G period because this is that the
pure in G and that will be equal to FG pure but actually what is the
definition of pure for composition of functions that\textsf{'}s exactly this
it\textsf{'}s a pure of F followed by lifted pyrimidine so it\textsf{'}s the definition
of what pure use for the function f G and so therefore the law holds
you now consider the identity function you know the identity function
is like this or sometimes can it can be denoted by it with a capital
I so this is identity factor I believe the cat\textsf{'}s library does this
maybe not maybe Scalzi so how do we define a sequence for it well
this is just an identity function because it doesn't do anything because
we we have f of a it goes to F of a because it is just wrapping it
doesn't do anything so this is identity function we could even write
this sequence function differently like this in order to underscore
that factor that\textsf{'}s just identity function now let\textsf{'}s check the laws
the identity law which is this now if F map is the identity function
sequences identity function f map L is just this F map L is the identity
function of its argument and because of this identity function and
so this is equal to f dot P so this is f dot pure followed by identity
and that should be equal to F dot penis clearly so composition is
that we have a sequence followed by F map of sequence now sequence
of anything is identity so it\textsf{'}s just composing one identity and F
map of another identity but we know that lifting F map of identity
is again identity so this is just about composing one identity or
another that\textsf{'}s always going to be identity so that is also identity
by definition and so this law holds let\textsf{'}s move on to the next construction
which is the product for any traversable factors G and H their product
is reversible now I'm going to introduce my own typeclass which reversible
just for convenience but actually the cat\textsf{'}s library has a traverse
that class but I just want to show that this is easy and I prefer
to define seek and they prefer to define Traverse in their tag class
so that\textsf{'}s why I have my own tie plus but basically this is very simple
that concept has just one method and this method is Elif a to FLI
traversal defined that method now this red is a problem with IntelliJ
and install a plug-in cannot resolve the types it compares this entire
code comparison works also we have a convenience method to get the
Traverse into instance this drove in the syntax to use seek as a as
a method rather than user so let me then show how I can define an
instance of track of travel this traversable type was for this type
constructor which is a product of l1 and l2 given that both l1 and
l2 are traversable factors so first time to mend the functor instance
well that is standard it\textsf{'}s just a map this map that just a functor
instance for product and then i implement the traverse instance using
C so what am I supposed to do I have this a1 F a times l2 FA and I
need to give F of L 1 a times Delta a so first I can say please so
sorry first I can sequence each of these separately because l1 is
reversible and all to escape most of my assumptions for a sequence
separately both of them then I can zip the results and I get what
I need so that\textsf{'}s my idea about how to implement so I just say sequence
the first one sequence the second one and zip now I could also write
the code like this but then my IntelliJ doesn't understand where these
things are coming from but the code actually still compiles if I do
that so this is just much more your boss telling me where the sequence
comes from from which factor and in principle I expect a scholar to
be able to derive this automatically and it can this is much simpler
to write about intelligent isn't like it so let\textsf{'}s check the laws here
so there is the identity law which is that we can map the pure and
apply seek and that\textsf{'}s the same as the pure so how do we verify this
law well we substitute the code of F naught which is up here and we
apply both sides of this law to some arbitrary value of this type
and one until two so we do that looking at the laws actually we have
to start from LA and the law will give me this so the value on which
I apply both sides of the law must be of type le so that\textsf{'}s why as
eleiza is a pair of L 1 and L 2 and then that\textsf{'}s why I take some arbitrary
pair and i apply the law to it so the left-hand side first i apply
this and that\textsf{'}s going to be that there\textsf{'}s a half map this is L 1 this
is no true and then we apply the seek function to this now the code
of seek is I'm going to write it like this in a shorter form and the
result will be that I have this seek zip this so now we need to assume
obviously that the law already holds for a 1 and L 2 separately and
therefore for example we have this which is the formulation of the
law for L 1 and so we can substitute that in here and then we get
that now because of the identity law of applicative zipping of two
peers is a pure of the peer so this equals F pure of the peer and
that\textsf{'}s exactly the same as applying F pure which is on the right hand
side directly to the pier so we have verified the identity law let\textsf{'}s
verify the composition law this is how we could write it I have written
out sequence seek of L seek of the hell everywhere it\textsf{'}s just for clarity
so in my notation that means a sequence made up defined for the tag
constructor L applied with respect to the type parameter F so now
let\textsf{'}s apply again both sides of this law to some suitable value let\textsf{'}s
see what type that value should have which you have the type L F G
C as the initial point in the time diagram so let\textsf{'}s have an arbitrary
value of type L F G C so sort of C values a here so L F GA naar betray
value of that is a pair of l1 f g l2 f g and applying the code for
seek to this we get a 1 FG a sikh with respect to f zip f l2 mg is
equal respective so that applying just the first step according to
the type diagram that would lead us in here which is f of LG F of
L 1 G 2 G so now we apply F naught F of this to that now what is f
naught F of CBG know seeing G is with respect to L sorry with respect
to G over L so it acts on some value of this type and it will give
this according to the definition but we need to lift this function
was F naught s the difficulty here is that f is an arbitrary function
we don't know what ethnic F does we don't have code for it we need
to keep it symbolic so clearly we need to use a definition of zip
F G somehow to find out what F naught F will do so the definition
of zip of F G is this there\textsf{'}s some FG x and f gy with zip them in
the factor F G so so have G X is a type F of G of X G Y is of type
F of G the definition of the zip for the composition is one of the
constructions for applicative it\textsf{'}s it\textsf{'}s a zip in the F factor followed
by F map F of zip in the G factor is this what we have in our formula
not quite because we have not just something zip F something after
which we we do F method but we have these things transformed we seek
so let\textsf{'}s transform using some function so let\textsf{'}s use a natural G of
zip so that we can transform like this so we transform under the factor
f and so the result is the same as if we transformed FG x and f gy
and then zip so that\textsf{'}s a natural T you can transform first and then
zip or you can first zip and then transform that\textsf{'}s up to up to us
so finally if we use this formula we can see that F map f of seek
L of G is like this it\textsf{'}s the F map F of this so this is seek L of
genii because seek L of G gives us this kind of expression which is
similar to this P of GX being sequence of this zip G and Q of G Y
is sequence of this and then we apply this to those things and so
the result is that F map of seek L applied to that is it\textsf{'}s like that
it\textsf{'}s sick F map sick G and then seek F maps engine so that\textsf{'}s what
we find this really apply natural TMZ so that\textsf{'}s the left hand side
of the composition and the right hand side is that so these must be
equal now the definition of seek F G is the code of seek that is just
applied to this type parameter F G instead of that F so the same code
and it would have been the same code if we could have this equal to
that now these are six with respect to factor l1 so these are defined
for l1 and these are defined for how to now we assume that for l1
l2 the composition law already holds so that means for example this
so this is the composition law for a 1 and similarly for L 2 so therefore
this is the same as this and that is the same as now and so the composition
law holds for hell the third construction is disjunction so for any
traversable factors G and H the disjunction is again a traversable
factor so we have seen an example of implementing this in either and
in polynomial factors but this is a general construction so let\textsf{'}s
see how to again we assume that factors l1 and l2 reversible and we
defined well as the disjunction of l1 and l2 a standard factor instance
but is Junction so now let\textsf{'}s implement the founder instance traversable
instance for the disjunction so here\textsf{'}s how it will work we have this
so we apply sequence to each of these separately we get this disjunction
and finally we depending on which one we have we lift it into the
F of disjunction using just constructors of the disjunction that left
or right so that\textsf{'}s how it works first we do a sequence on each of
them so if we are on the left and we sequence it again this and then
we map it with left apply which means that we put a left on top of
this and left it\textsf{'}s just a wrapper in a disjunction so it doesn't change
the value and the same we do for the right now the redness here is
again due to limitations of IntelliJ it\textsf{'}s unlabeled transferred types
directly but this code runs it compiles and runs let\textsf{'}s check the laws
at the entity law we do the same thing as before we just substitute
the code of the flap in here and then we apply to some LA we'll know
that both sides of the identity law applied to an arbitrary element
of this type now since the code is symmetric with respect 1 or L 2
it\textsf{'}s sufficient to apply this to some left of l1e and check the law
for that so if we apply it to the left and we are in this case we
have any left applied to to this which is well we are actually in
this case and we're looking at F Nobel first so we are you want to
lift like this now you notice we can't really simplify this because
these are map and pyramids of factors that we don't know these are
a one factor and if I look at your factor so we don't really know
what these methods do we cannot substitute any more code so that\textsf{'}s
our symbolic computation right now we apply sync to this now we're
on the left so we apply seek to to this which is I'm going to denote
that a seek l1 to that and {[}Music{]} followed by map of left block
now nothing more to simplify unless we use the fact that l1 already
has this law and so this law for l1 looks like this therefore we can
simplify here substitute that we get F P were of l1 a map left apply
which by naturally T appear and we have pure of left over one a and
that\textsf{'}s exactly what the right hand side will do when applied to left
of l1 e so identity law holds let\textsf{'}s consider the composition law the
composition law needs to be applied to a value of this type and again
it\textsf{'}s sufficient to consider the left and applied to that so first
we apply the seek and that gives us in this now we apply f map F to
belt and we notice we have F map F which is this one and another if
map F so we can combine them and the result is that we have this two
which we apply map with respect to F of this kind of function so we
first do we left apply to that and then we further apply this function
so now this is not quite Scala code because I have this map underscore
F for convenience and clarity so that\textsf{'}s just keep in mind I'm not
actually using your Scala code here but I could adjust that the types
will be less clear so now what does this do now this c g you know
seek g has to act on the left and we need to substitute the code of
seek when acting on the left it gives us this expression my definition
of our seek up here so let\textsf{'}s substitute into this and we get then
this expression so now we can use the composition law that by assumption
already holds forever so then we have this one Perelman which we can
rewrite like this now this law is not quite giving us the expression
that we want which is this expression because we have this function
here but here we have another map so we're not we have another left
apply to map and also on the right hand side of the law would have
another left apply so in order to put another map inside the seek
we use a net reality of seek we add this on the right-hand side which
gives us this seek so seekers natural so we can apply seek to a transformed
argument or we can apply transformation to the result of seek and
so then if we define what lab FG is that is f map of F map and we
put that onto the left-hand summit so that we have CK one of this
map F of this map F both of that you know we can combine the map F
this one with this one and now we have a single map F with a bigger
function but that\textsf{'}s exactly what we had for the left hand side and
kill him before and so therefore the right hand side response is equal
to the left hand side his code so the code is equal and the same would
be if we replaced a woman so this shows what laws hold for injunction
now let\textsf{'}s consider there is construction for which is a recursive
function defined as la equals some s of a and la so as s is an arbitrary
by functor so this could be any type function of two type parameters
and this equation this is a type equation it defines a type la recursively
so examples of this are lists and trees different factors s can encode
very easily different kinds of wastes and trees now this also describes
infinite lists and infinite data structures and we have seen an example
where the infinite data structure does not actually work you can implement
the function without the recursive calls never stopped so that\textsf{'}s the
problem the laws will appear to hold in our proof but actually it
will not work in practice so I will comment on this when I use the
recursive assumption in the proof so let\textsf{'}s see how it works so I introduced
the biofilter as a type parameter up front so that I don't worry about
it so much it\textsf{'}s easier in Scala to do this now I cannot just introduce
a type like I did here because reclusive type illnesses are not allowed
in school so I need to introduce your class so once that actually
makes the code a little clunkier because now and you need a name for
the data value inside and I need to wrap and unwrap but that\textsf{'}s a small
inconvenience so the class contains a value of type s of a end of
the same 11 so this is a type function that I'm considering as a parameter
and now I can implement a factor instance for this now this obviously
is going to be recursive so in order to map this l 8lb i map a to
be here and I need to map this la to L be recursively by using the
same map so I need to do this under yes so I need to map at the same
time a to b and le to l be under the type constructor s so that\textsf{'}s
by map so I'm mapping the two type parameters of s at the same time
and then my map is a method that takes two functions with two type
parameters so it goes a to C and in this case we have the by factor
with type parameters a and L of a and so it takes two functions a
to C and elevate to D gives us FCD so this is combining map with respect
to the first router and map with respect to the second parameter in
a single call which is completely equivalent to doing first the first
type parameter with a map and then the second parameter with another
map but it\textsf{'}s just easier to do it with one method probably two and
this is the recursive call to the same function so this is how we
do it the functor instance now let\textsf{'}s look at the Traverse instance
how would that work so L of a is the same as recursively defined as
s of a and elevate so now we need to transform this into this if we
want to implement seek how do we do that well we can obviously seek
here recursively so the second argument of s is a recursive instance
of the same type and so we can assume that for that recursive intense
instance we already have the implementation so that would be the recursive
call to the same function so that would be transferring into Fla so
now we have so we just do a by map where the first one doesn't do
anything it\textsf{'}s identity and the second function is a sequence recursively
calling the same and now we do by Traverse or by sequence actually
by sequence which is as I indicated before it\textsf{'}s transforming s fafb
into F si be pulling out the F at the same time out of both type parameters
to the outside so we use that and transform s of F a Fla until F of
s of any LA so this is exactly what we need so in other words seek
is just a composition of by map and by seek but on that one factor
now I can use cats library it has by functors by traversable and it
has this voice sequence so I'm using white functor and white reverse
which is canceling berry typeclasses just I could have defined them
just as easily as the trove that class and the redness again is a
some problem with types although I indicated all types explicitly
but still it doesn't like it so therefore the Seekers just by map
with identity and seek which is a recursive call followed by the by
sequence call on the by factor so that\textsf{'}s exactly what we plan to do
first we buy map so that we seek under yes with respect to the second
type parameter and then we do by sequence yes so that works and let\textsf{'}s
check the laws so the identity will need to substitute the code now
for for clarity I still write f9l here and so on but it is easier
now to distinguish sequence with respect to L and s because s is a
by function so it has basic and violent and L has seek so I'm going
to write seek L I could have done it like this but I'm not going to
write it for quality for brevity so okay substitute the code of f9
that gives us this code which we defined here the lab instance the
defunct our instance for help which maps using by map under F and
the recursive on the second so let\textsf{'}s write it down so this is a by
map of this function and the recursive FF L as a second argument of
why map so the same function as we're defining here is here so now
we need to apply secrets the result is this followed by by map actually
followed by bicycles remind myself what is my definition of sequence
for you yes just take the S out of the case class which I'm not going
to write here because it\textsf{'}s just wrapping and unwrapping we want to
pretend that this case class is just a type so first it\textsf{'}s apply map
with identity and seek and then it\textsf{'}s a buy seek on the result I'm
going to ignore this because this is just wrapping right so seek is
by map followed by by sick this is sick L so we have this expression
now we can combine the by maps just like we can combine maps because
they're by factors it\textsf{'}s just first we have a map in the first type
driver so we combine these two which gives us this and then we have
a map in the second type planner which combines these two and that
gives us that so f map L and then seek is the same law that we're
trying to prove not F not LPR and then seek is f pure so it\textsf{'}s a recursive
invocation of the same law and we're trying to prove in the second
function of Y map so we can use an inductive assumption that we already
proved that by recursion and therefore we just substitute into this
expression we substitute F P R inside of this because that\textsf{'}s a look
so then we get by map of pure pure by seek and the identity law for
s means that s by map pure pure basic is the same as s is just pure
and so that\textsf{'}s wasting holds for Escalades by traversable function
by function and so this becomes the right-hand side of the identity
law and that\textsf{'}s the proof of the identity law so now let me mark about
using the recursive calls and it is that inductive assumptions corresponds
to recursive calls in code so in mathematics the inductive assumption
is that on the previous step things were already proved in code it
means that we are going to call the same function recursively assuming
that it will return the correct results then our step also returns
the correct results but that assumes that the recursive call terminates
and actually returns the results and we have seen an example that
on the infinite list it does not return it has anything to do and
so that\textsf{'}s where it is going to break so actually the inductive assumption
can be used as long as all these functions actually terminate their
evaluation and return their results and if so then it\textsf{'}s off it\textsf{'}s all
fine but so at this level we will not see any problem with infinite
lists we are using the inductive assumption and everything appears
to be correct however we have not established that these functions
will actually return at all and for the infinite list they don't and
so for some factors defined using this construction using some by
factor s some factors will have infinite loops and others won't so
that is a separate thing we need to establish in order to check that
they are actually reversible this is usually not a problem for factors
because this map is going to be cold maybe later and this is a lazy
call and so there is no infinite loop but we have seen we do a bye
map and then we do a buy sequence and so that call will evaluate everything
and that will break for the infinite list now all I'm saying is that
this proof of laws and the same will apply to the proof of the competition
law that I'm going to talk about shortly this proof is only as good
as the fact that all the functions return and if you have an infinite
loop in one of the implementations then as proof oh well great because
the inductive assumption cannot be used because the use of inductive
assumptions is is translated into recursive calls in the code and
if those goals never terminate them you can't call them so I'm not
going to present an analysis here as to what possible functors s are
admissible because I don't know how to do that analysis in general
so and that\textsf{'}s a much more difficult topic of recursive types what
are the reclusive types for which certain methods would terminate
and that\textsf{'}s for another chapter so from now we will assume that we
check separately that all the methods will terminate and if that is
so then this proof is correct we are allowed to use inductive asymmetries
let\textsf{'}s look at the composition law so this is the composition law and
the law is an equation both sides of which need to be applied to an
arbitrary value of this type let\textsf{'}s check so L F G C so use a instead
of C I'll probably check rank it in the slides that it is a and not
C I'm using a in the code consistency so s of F G a L F G so that\textsf{'}s
lfg so let\textsf{'}s apply both sides of this law to some value of this type
and we get first sequence which is by map of identity and sequence
followed by by seek and then we do a map of seek which is a function
that takes this and does a by map and and by seek but now with respect
to G so I'm just writing it out what the code is for seek and this
should be equal to by map for the advicing but with respect to FG
so that\textsf{'}s our law let\textsf{'}s check that the schools and we certainly assume
that it already holds for for the s by function which means that this
equation holds and by seek map is by seek now this is just a law this
twisted composition of seek can seek is seek so how do we use this
in order to prove this now clearly to use this we need a value of
this type which is not the same as what we have here now this is s
FG x FG y so is very homogeneous it must be the same functors FG and
we don't have the same factors here we have F G and L F G so this
L is outside if L were inside of all of this here then we could just
say this is why this is eleve is why a is X and then we are of this
shape so that means we need to permute L over there so in order to
do this we need to sequence this with respect to F G and then L will
get inside but we need to use the sequence inside the type constructor
s which requires a buy map now this is going to be a buy map with
respect to the second type parameter of S which is the recursive invocation
and so that by map and sequence is a recursive call to sequence therefore
we can use the law of composition for that as if it\textsf{'}s already proved
and we will do that so here\textsf{'}s what we do so in this law that we are
going to use now we're substituting this value s FJ XY which is defined
like a by map or a sequence with respect to L and respect to F and
then G and then that\textsf{'}s of the right shape with X equal to a and y
equal to L of a so that\textsf{'}s what we wanted and the result is this expression
which is a by map followed by by seek followed by map now we can certainly
use natural reality and exchange map sorry no we we here we're having
basic F map by CG that\textsf{'}s what we're using here it\textsf{'}s a basic FG that\textsf{'}s
that\textsf{'}s the law we're just writing out the law we're substituting s
F G X Y into both sides of the law services here and this is here
so this holds this is an equation that holds so now by inductive assumption
a composition law for sig L already holds when we use it here and
so therefore we can rewrite this right-hand side like this this is
just sick L of F G now this right-hand side is the same as the equation
that we need to check which I noted as a start and just marked labeled
that equation by start for convenience so the right-hand side of that
equation is now the same as this therefore it\textsf{'}s also equal to that
so it remains to show that that the left-hand side is equal to the
left hand side of star let\textsf{'}s write it down so like this yeah it\textsf{'}s
really easier to compare so by map now we have this instead of that
and we have a by seek and we have a map of by seek instead of this
now if we look carefully we have a map f of by seek and here we have
a map f of something that\textsf{'}s followed by by 6 so that can be pulled
out with a map F and omitted so this is a training lab F by sake of
G in both of these so as we just a minute forget this so now the problem
that they are not equal because we have a different order of by seek
and map so have a by cyghfer by map here and here we have a map followed
by by seek when we need to interchange a map and the natural transformation
that\textsf{'}s naturality law and it\textsf{'}s the same way for by factories just
by secant by map can be interchanged let\textsf{'}s write down the naturality
law for clarity it looks like this so we have a basic follower by
map f of by milk of something and then we have a by map of map f of
that function let other functions we have two functions because by
map takes two functions both of them need to be mapped and then we
have bicycling so we have interchange the order by seek and map f
so if we use this law in this equation then we get that the first
line is equal to again we can interchange by c combining up and we
get by C cadine so now we have by map followed by by map followed
by by seek by map can be combined and then we have this by map fold
but by seek and this is exactly the left hand side which is this emitted
by C kanji sorry this one so this concludes the proof of the composition
law and therefore we find that this construction was valid now the
question is which by factors are by traversal and the answer is the
same all polynomial by factors are by traversable now we see without
recursion these constructions 1 2 3 our constructions that allow us
to get any polynomial factor with arbitrary types in it doesn't have
to be monoid like in applicative can be any any constant type any
polynomial function these constructions cover all these cases now
construction to even has two different implementations we can zip
in one order or in the opposite order it still will work and therefore
all polynomial functions at reversible now exactly the same constructions
worked for by traversable constant and a and B are quite reversible
in the same way as constant an identity function traversable and products
and disjunctions are by traversable and so-called by traversable polynomial
by factors can be used in this construction I'm not going to go through
proofs for these by functor constructions they're pretty much the
same as the proofs I went through except you have more type parameters
to worry about what implementations are exactly the same and so the
conclusion is that all polynomial factors including recursive polynomial
factors as long as the Traverse and seek methods return in finite
time and they not go into infinite loops as long as that is the case
all polynomial factors at reversible all polynomial by factors also
traversable and you can go on you can define a by factor by recursion
using a try factor in the same way you can say sa B is equal to some
T of a be s a B or T X Y Z is a try factor and as long as that try
factor is tried reversible exactly the same proof would show that
the by functor is by traversable so you can have recursion at any
level as long as it\textsf{'}s a finite level of recursion obviously at some
point you would have some n factor that is not recursive recursive
and or maybe several of them and then as long as that\textsf{'}s polynomial
is going to be 2n traversable and then you go back and have your n
minus-1 traversable recursive thumpers and so on and so it\textsf{'}s clear
that all polynomial factors with arbitrary recursion so it\textsf{'}s it\textsf{'}s
a tree for example whose branches can be themselves lists or you know
you can have a list of branches or anything like that all of that
is traversable so that\textsf{'}s a major result of this consideration so now
let me consider foldable functors now we we know the fold operation
in a standard library it\textsf{'}s a full left turns out that the fold operation
is a consequence of having a traverse operation and later we'll also
see that the scan operation the scan left is also a consequence of
traverse operation so how do we derive the fold from jurors the main
idea is that we should take a specific applicative factor which is
a constant factor fa equals a constant Z or is a Z is a monoid type
and so the zip operation on this factor is just a monoid operation
which I will denote like this and we have seen in Chapter 8 that these
are applicative now the type signatures are much simplified now in
type signature of triggers becomes this and this method is called
fold map well the does is that it takes a container of type of values
of type II and takes a function that map\textsf{'}s each value to a mono it
and then it traverses the container and combines all these monoid
values into one big monoid value and that\textsf{'}s for example aggregation
and any kind of aggregation Sun Oven integer list or some pointer
so the general method with an arbitrary monoid which is generic in
the monoid is called faulkner the type signature of seek becomes simple
like this so and that is just to concatenate all monoid values in
the container into one using the monoidal operation so this is called
M concat now there aren't any more laws because the laws are about
combining oh the identity law will be automatically satisfied and
the composition law is trivial because you can't compose these things
because there is it takes two more nodes compose them you get the
second one the first one is just just going and so all these laws
are trivially satisfied there aren't any laws anymore for this foldable
operation for the fold map there aren't any laws and all traversable
functors have these operations now nevertheless it\textsf{'}s convenient to
define the foldable typeclass that has these operations like fold
map and M concat and fold left because you could traverse the containers
in different order and that would be different implementations even
though there are no laws and it\textsf{'}s basically a consequence of traversable
so there aren't any factors that are foldable but not reversible so
all polynomial factors and only the polynomial functions are both
foldable and traverses and and so nevertheless it\textsf{'}s convenient to
define this typeclass because you can have different implementations
of fold for different order of the traverses and finally let me show
how to define the fold method and that\textsf{'}s a trick where you take this
as your manual type now this is a mono eight where B is an arbitrary
fixed type and these functions are just concatenated by composition
and the identity value is the identity function now if you substitute
into the following up into this substitute B to B you get this type
signature it\textsf{'}s a curried function with one two three arguments so
if you just rearrange these arguments you see this is exactly the
type signature fold left it has your container it has initial value
it has the update function and it returns the final accumulated value
so monoid is gone we have a specific one right here the arbitrament
already that is is gone until we have an arbitrary type B so if we
put B before this argument and it\textsf{'}s not obvious where the money went
but it is just a consequence of a signature of Traverse where we first
put them on oil in it and then you specify to this node and so for
this reason every foldable has a foolproof method for map and M concat
and every traversable also has them and so now we know which factors
are foldable and reversible so let\textsf{'}s ask our contra functors useful
or profanity was useful in the same capacity because you could imagine
that you want a conscious factor that you Traverse with respect to
a function or my servers and my answer to that is after several analysis
is that they're not very useful here\textsf{'}s why let\textsf{'}s take a contra fantasy
now let\textsf{'}s try to do a seek on it so that would be this kind of time
signature now if I have a CFA I can control map with the pure method
the pure F which is a to FA I can come up with that to get CFA to
see a so I can get down and then I can put that into the F using pure
F so I get F CA and in fact there is no other way of doing this generically
now it seems that wall control factors are automatically reversible
and I could even say F doesn't have to be a factor it\textsf{'}s not using
map well if I'm just using pure life and so it\textsf{'}s it can be arbitrary
Pro functor as long as it has pure it\textsf{'}s actually applicative proof
functor or even just appointed with a pure so it can be just just
like that so is that useful well in my view it\textsf{'}s not useful because
I completely ignore all effects of EV I'm using pure of F so whatever
F ahead here I'm ignoring its effects I'm never going to have any
effect full value here either it\textsf{'}s going to be always a pure so it\textsf{'}s
not very useful and in the other direction you can't do it f seiei
to CFA because you can't extract out of F necessary now if you have
a proof factor see anything things are not workable here\textsf{'}s why consider
this simple example a simplest growth factor just neither a functor
nor control factor because it has a in both covariant and contravariant
positions now we need a sequence function of this type signature but
that\textsf{'}s it\textsf{'}s it\textsf{'}s impossible we cannot get an F of a to a unless we
somehow get an a to a first but we can't there\textsf{'}s no way to extract
a to a out of here so I can't get an A you can't get an F of a and
so there\textsf{'}s no way to do this so so the only way to implement this
type signature is to return pure F of identity here but that ignores
its argument and functions that ignore its argument will not respect
the identity law they will not preserve information and finally let\textsf{'}s
try to try to traverse profile too with respect to proof hunters and
we find again that the only way to do that is to ignore all effects
here are two examples so consider this contra factor and this contra
factor then now if it\textsf{'}s applicative it means that s is a mono it and
so this type the only way to implement is to return an empty value
of F on the right ignoring all of Fame and the second example is you
take this contra function and this function and again you can show
that the only way to implement sequence of this type signature is
to always return empty option and again that would ignore its argument
and so it\textsf{'}s most likely you're not going to be useful because we ignore
all the effects will never return anything that\textsf{'}s not empty and so
on so we we are able to implement these type signatures let\textsf{'}s see
I have I have this test code here for a check that we can actually
implement only one type signature and that it returns an empty option
in both of these counter examples so take a look at this in more detail
if you feel like but I'm of the opinion right now that since all of
these examples show that I have to ignore all effects I have to return
a value that ignores all the input data or ignores all the effects
in the factor or per factor f that\textsf{'}s probably not a very useful implementation
but there isn't any other also note that the laws of jurors suppose
the notes actually say that effects of f cannot be ignored they don't
actually say that so you can traverse each element once and that\textsf{'}s
guaranteed but then you can just ignore the effects maybe well for
some functors that\textsf{'}s possible as we have just seen so the conclusion
is that traversable contractors and pro founders aren't really so
great and aren't very useful let\textsf{'}s look at some examples where we
use traversable factors the first example is we can convert any traversable
factor data structure to a list to do that we will actually have a
trick and that will all define a list as a monoid not as a type constructor
is a constant type but as a monoid so it will be a constant factor
so to express this i define the type constructor z which has a type
parameter b but it\textsf{'}s equal to list of c or c is a fixed type parameter
up here so it\textsf{'}s not depending on B so this will be a constant factor
which are defined like this so it doesn't change anything the type
parameter is not used and it\textsf{'}s applicative as well as a constant for
a factor that is a monoid so I define the evocative instance using
the rajab and this is an eel and a monoid composition or concatenation
of lists and just for fun I want to define the monoid composition
in the opposite order {[}Music{]} so having defined this and now have
Z as a applicative factor and I can use chillers which is this function
that I defined for convenience on the reversible value and so now
I Traverse F of a which is this L of C probably better cold now this
L of C is of type unknown type constructor hell so we Traverse it
with a function that takes a value of type C and returns a list containing
a single element C the result of traversing is that for each element
from the data container L will have a list of a single element and
then we will concatenate all these lists because that\textsf{'}s the effect
located factor Z and we need to combine all these effects for it all
values in the container health and the combining is done using the
monoid composition and so then the result will be a list of all elements
from the container l so let\textsf{'}s see how that works we define L like
this we have seen the implementation already and now we define a value
of this type the value is triple 1 2 3 and then we did recall to listing
it and the result is a list of 3 2 1 because we have defined the opposite
order here so if we define a straightforward order we would have a
list of 1 2 3 otherwise we have a list of 3 2 1 so in this way we
see that any traversable factor is a data container that can be converted
to lists and the order of list elements depends on the order of traversal
which is specified by the traversal hibiclens instance the second
example is to aggregate data from a tree by using a fold so in fact
since fold is an operation of traverse where the negative factor is
a constant factor here we have just used fold map essentially we don't
need traversable here we it\textsf{'}s efficient to have foldable we could
have defined this function by folding with with a list but let\textsf{'}s continue
using traverse just so that we understand these are very much related
to each other so here\textsf{'}s a definition of a simple tree tag it has a
leaf of type A and it has a branch with two trees now we define the
function instance in the usual way and then we define the traversal
industry which is defined also in the usual way this is a recursive
construction construction for and so I'm just writing it out this
follows from the recursive construction if we have a leaf and we just
put the leaf constructor under F and if we have a branch and we run
sequence on both branches this is a recursive call to the sequence
function that we're defining right now and then we zip the results
and put the result in to pull under the branch here are some example
values of this type so this is a tree of integers and this is a tree
of strings and I driven this picture to visualize this tree t2 has
a more complicated structure T 1 is just 1 2 \& 3 it\textsf{'}s easy to see
what T 2 is not so easy to see anymore so let\textsf{'}s fold over T 1 so T
1 is 1 2 3 in order to fold let\textsf{'}s define a 1:08 for integers which
will be a multiplication and what\textsf{'}s the fold map with a function that
squares each element so the result of fold map will be the product
of squares of all and of all the elements stored in the tree which
will be 1 times 4 times 9 which is 36 the third example is to decorate
a tree with order labels obtained from a depth-first traversal so
for instance this tree if we Traverse a depth first then first we'll
reach a and we'll reach B then C and then D so then the order of traversal
is 1 2 3 4 and so we expect these labels to be attached so how do
we attach labels like this way it\textsf{'}s not just a map map would we can
certainly attach constant or a function of each of the label each
of the element but that\textsf{'}s not we won't want to attach a value that
depends on the traversal so that\textsf{'}s the Traverse and since it depends
on the traversal we need to compute it as we go and so that\textsf{'}s I mean
we need to maintain state as we go as we traverse the tree and maintain
in the state can be done with the state monad so we use that statement
others duplicative function and that expresses the effect that we
are traversing with so to visualize this traversal I could say that
we are first so let\textsf{'}s Traverse t2 since we have it on the screen so
we first Traverse t2 by visiting a and we have some function that
takes a and returns a monad value or a purgative function value in
general now we done this being and we combine the effects so we have
four different effects in these four different a purgative functionaries
we need to combine them using zip and so the result is an F of tuple
of a B here and then it\textsf{'}s going to be this nested tuple so it\textsf{'}s f
of domestic tuple and then we have to recreate the three structure
out of that nested tuple by remembering where these a B and C and
D were in it in the tree and we have to reconstruct a tree under F
so this and I'm not going to write much more detail with basic analysis
so it\textsf{'}s to be reconstructed as the value of this type after after
zip and you would just have an F of some tuple and you could have
converted it to a list first but then you completely lose the structure
of the tree so the traverse operation must somehow keep track of the
structure of the continue and you recreate it after zipping so it
zips the effects so the effects are combined linearly in the traversal
order using the zip and then after the effects are combined effects
are mono it always of some kind so they are combined linearly there
is no tree structure only effects but there is tree structure on the
values ABCD or whatever values you get after you transform them with
the function f and so those values have to be arranged so that could
be of type B those values have to be arranged into the same tree structure
as before so now we are going to use a state monad as the positive
effect and statement others applicative and you will use if statement
values together what happens is that you update the state each state
mullet value could update the state in some way and so this is a linear
sequence of effects that you need to combine by updating the state
first using this updater than using this updater and so on in the
linear order of traversal and that\textsf{'}s what well we will use now we'll
have a monadic value make label so we define first of all a state
monad I'm using the Katz library with integer state so for convenience
I'll call this s right now just in this test so I'll I define a make
label value which is a monadic value that updates the state and returns
also this value that is the previous value before I'm dating I could
return the next value it doesn't really matter and that\textsf{'}s going to
be melodic value that we are going to produce for each of the elements
of the tree now we actually need to represent this as an applicative
factor so let me just quickly convert to my zip typeclass which is
my my version of applicative of course the cats library already has
a positive instance for this but it\textsf{'}s easier to use my my typeclasses
because they're very small they don't have a lot of methods and it\textsf{'}s
easy to see what they do so we need to define the wrapped unit which
is just a pure of state factor and we need to define zip which is
defined in a regular way for anyone that this is just combined the
two effects in this order we could have changed the order here so
this is this is a freedom but let\textsf{'}s just keep this order and this
function will allow us to produce her with zip tie plus instance from
a statement well you know what\textsf{'}s right a tree traversal so a tree
traversal we already implemented up here so I just copied this code
in I don't think I needed to duplicate nice code we can just remove
this code so how do we use that so we have t2 which was defined before
that we Traverse using the effect type yes so this is the apocatip
factor that we have now a wizard instance for we have this was a probe
s and the result type is going to be a tuple of string int so we're
adding an integer label to a string type of the tree which which t2
has 32 think and the type is tray of string so the function with which
which reverse takes a label and prefer this make label operation which
is a monadic value and then we map now this magnetic value returns
the integer and then we map that integer into a tuple with the previous
tree leaf is really called leaf action to be more clear so we map
a tree leaf to a tuple of leaf and label and we get out of the Monad
so now this is a value of type s of tree of string int so this is
a result of traversal and now we need to run it so we run the statement
out on the initial value one and we extract the value out of it so
this is that cats library API two is to extract values from statement
and the result is as expected so it\textsf{'}s a labeled with 1v we still in
soon so in this way we can decorate the tree with labels that are
computed as we go on in a traversal the next example is templum and
skin functions scan map and scan left so we have seen that fold can
be implemented if you have it reversible and scan also follows from
properties of traversable so scan map is something I made up it\textsf{'}s
a method analogous to fold map where you have a monoid and you map
your data to a monoid type and then the result is that unlike fold
map it\textsf{'}s not just one monoid value that aggregates everything you
don't just accumulate the final value you keep all the intermediate
accumulated values and put them back into your container so this is
like the scan function so how does it work we use a statement again
it\textsf{'}s state is the MU node so initially it will be empty and then we
will accumulate a monoid state so this is how we accumulate we get
the previous state and we set the new accumulated state and then we
get again in new states so that we have it on hand and then we Traverse
with a function that is f which is this given F followed by accumulate
and so the result is s of Z which is a state that accumulates Z and
also gives it as a value so after traversing we get a value of type
s of L of Z\textsf{'}s and then we run it on an initially empty value and that\textsf{'}s
what we return extracting out of the state monad after we have run
it so here\textsf{'}s the test let\textsf{'}s use a string as monoid so we imported
a cat\textsf{'}s instance just for standard string 108 and let\textsf{'}s do a scan
map on t2 with no transformation so then we're just going to accumulate
the string as we go so we get a a b a b c a b c d so that\textsf{'}s the result
of scan map and we can also implement the standard scan left function
which is very similar except we don't accumulate a monoid now we just
accumulate a value of some arbitrary type z and we do the same thing
as we did before very similar code and here\textsf{'}s a test so we let\textsf{'}s accumulate
the length of strings in the in the tree so then we'll get one two
three four because all all strings have length 1 and the last example
is the traverse a rigid tree or non monadic tree as I don't think
vegetation well it is a widely used word to describe this kind of
tree but basically imagine a tree that must have all branches fall
so it cannot be unbalanced then it must be full it\textsf{'}s a binary tree
that must have one two four eight 16 32 and so on elements and no
other number of elements can be in the tree that\textsf{'}s very rigid in its
shape this recursive type equation he finds it and you can easily
see why so it\textsf{'}s either a or it\textsf{'}s the same T of any times a so then
it\textsf{'}s either a times a or the same tree of a times a times a times
a so then it\textsf{'}s for A\textsf{'}s or eight A\textsf{'}s or sixteen is consumed so it\textsf{'}s
it\textsf{'}s at this infinite disjunction with 1 a or 2 is 4 4 8 or 8 8 and
so on so that\textsf{'}s that\textsf{'}s why this equation works not we don't have a
construction where I did not write down the construction that can
generalize this tree this kind of construction could be generalized
like this where you have a recursive equation with some buy furniture
yes and the second type 300 - 2 s is not a la as it was previously
not just LA but it\textsf{'}s L of some RA where R is another function so in
this case it will be a pair but in general it could be some other
function and that function must be both applicative and reversible
and if so then I believe if this construction will work as well so
this is a more general recursive construction let\textsf{'}s see the code for
this so the definition of the tree type is this it has a single element
in the branch which is a tree of the pair parameter instead so we
substitute to the type parameter which is kind of non-trivial so we
can define the functor instance which is a bit of work because now
we need to map this branch of type 3 of a a we need to map it recursively
with a function that map\textsf{'}s a a to be me but we don't have that function
we have a to be so we need to construct a function that map\textsf{'}s a a
to be B out of F and the traversal is again a depth-first traversal
where the leaf is handled the same way as before but the branch is
handled differently because we actually have this kind of type and
we need to get this so we need to do we need to use zip for F in order
to pull F out of the tuple and so we first zip the FS together like
this and this needs to be done under the B so it\textsf{'}s a b fa fa map of
the zip so that\textsf{'}s going to have B of F of praa and then we sequence
that so we get F of of PNA and then we wrap it into the branch so
that\textsf{'}s how traversal works and certainly we tested you know this is
how we would create this data structure so it\textsf{'}s always branch branch
branch branch and finally leaf with a very large may be nested tuple
so this is why this tree is so rigid he does not have cannot have
unbalanced shape so that works we use in mono omoide instance for
integer and do a fold map with identity to get the sum of all these
numbers so these examples indicate that we can do a lot of things
with Traverse but there are there are actually things we cannot do
using each others because the Traverse separation we remember it is
an operation that needs to be generic in the effect against which
we Traverse in this applicative factor so two things that cannot be
implemented the traversal which you find interesting but this is so
or the breadth-first traversal for a tree so imagine a tree of this
shape and you want to do breadth-first traversal so you traverse first
at this level you get one and you traverse at this level you get to
an elite reverse at this level now that can cannot be expressed as
a traversal with some effect because as I indicated here to visualize
a traversal we need to imagine that we are computing a large linear
sequence of effects into one combining a large linear sequence of
effects into one big effect and now in order to express this you would
have to have to know for example here that this two must be two and
not one now this effect cannot come from just recursive traversal
you cannot just take a usual recursive depth first traversal and run
some more nuts and clever Monat with it and get this other chamber
so now we certainly probably can implement it in some other way but
I don't see how you can simply do a recursive function on a tree that
traverses it against an applicative factor and get this effect and
especially when you call recursively on this subtree you need to know
how many nodes will be in some other levels in some other subtree
so it\textsf{'}s not clear how you could possibly get that information from
any kind of monitor or {[}Music{]} applicative function now certainly
you can implement breadth-first traversal but what I'm saying is that
you cannot take some special monad and some recursive function calls
and implement it so easily I hope you can still implement it in some
way that is not too bad as a traversal certainly the standard way
of implementing breadth-first traversal to use a queue or you in queue
each node and then you in queue it to children and then you DQ and
as you dqu in queue more so that can be certainly done in a statement
that that computation but the problem is you need the traversal which
recreates the original structure so if if all you want is twofold
then you can implement fold in a breadth-first while using a queue
like that but what you need is to recreate the original tree structure
and that\textsf{'}s very cursive structure that has a depth-first logic to
it and so that\textsf{'}s the difficulty and certainly you can do it with a
lot of extra work it\textsf{'}s not just a couple of lines of code like it
was for depth-first traversal so at this point I don't have code for
this maybe this can be done in some clever way but I haven't found
it and the second thing that I don't think you can do is to label
depth of the tree using a traversal so again it\textsf{'}s a similar problem
that effects so these aren't going to be effects and obviously you
need some kind of state to hold this one and then update it to two
and two three but effects are concatenated linearly and so it cannot
be that this three is the same as this you cannot avoid concatenating
this effect with this one when you do a traversal because of this
linear nature of combining effects and you cannot avoid combining
effects during traversal and so there\textsf{'}s no way to skip incrementing
the counter when you do choose ourselves so I don't think you can
easily express this kind of labeling and this is trivial to do ad
hoc as a function on a tree but what you want is to have a generic
traversal which is generic in the factor f and just uses the zip and
combines the effects and that\textsf{'}s why traversals are not so flexible
you cannot avoid incrementing your counter you cannot have logic that
says oh here I don't increment because they're at the same level can't
have that logic you must combine the only factors together so I keep
talking about being generic in the function f so let me talk about
it in a more rigorous manner so what we're looking for is to be generic
in the sense that the code for traverse as well as the code for the
sequence in it should not depend on a specific function f it should
only use the methods P R and zip or maybe map as well from F and {[}Music{]}
recall recall how we dealt with a similar problem when we discovered
founders so a factor is a data container that is generic in type of
the data that it holds and the map function or F map is a function
that cannot use specific type information about A or B it must manipulate
this data blindly with no change you take a container you take each
element a very replacement may be and put it back at the same place
but you don't know what types those are and so we expressed the law
of natural T for various functions by saying that F map should come
should commute with those functions so you can transform first or
you can transform later and that\textsf{'}s what it means that it\textsf{'}s generic
in the type of data so similarly generic in the function f means that
if we map a functor F to some other function G then a traverse with
respect to F will be mapped to the Traverse with respect to G so we
need this mapping somehow so this cannot be this can be formulated
mathematically I don't want to spend too much time on this but I just
want to mention this is an important mathematical development perhaps
but this is the first time where we have seen this kind of thing and
we don't have I don't have good notation right now for this natural
transformations between applicative functors and its need to be considered
so here\textsf{'}s the mathematical formulation we consider - Lickety functors
F and G and we consider a natural transformation between them such
that it Maps period of F into pure of G and it maps zip of F into
the project and then we demand that it also should map the Traverse
of F into Traverse of G so if we do that well all we do is we just
say we have a traverse with respect to F let\textsf{'}s apply it and then map
F to G in the result because the result of Traverse is F of something
F of some L of a or L of B so we can map that into G of not using
the natural transformation or we can first map f to G and then apply
Traverse and that should be the same and so this is a natural T with
respect to the functor as a type parameter so it\textsf{'}s a higher-order
type parameter itself otherwise it\textsf{'}s quite similar to not two naturality
and it\textsf{'}s just more complicated because it\textsf{'}s not just any natural transformation
natural transformation by itself has laws already and in addition
to being a natural transformation it needs to preserve the implicative
properties of f so that pure is mapped to pure zip is mapped to zip
and and the laws of course must hold for both implicated factors so
if you look at this notation which is slightly made shorter on purpose
by omitting various type parameters it really looks like lifting from
a function f to G into function of traversing you have to traverse
G but F and G are not types they're type constructors so and this
is not a function this is a natural transformation which is more complicated
object so when we used category theory to describe such liftings we
would usually say this is a morphism in one category and this is a
morphism in another category but a morphism as we define it was always
between two types now we don't have types we have type constructors
so we need basically a morphism between type constructors so that\textsf{'}s
more more precisely between implicative factors so a morphism between
applicative functions that\textsf{'}s what we need to lift into a morphism
of traversable faculties and so that requires a more general definition
of category than what I have given so far we're in them in the definition
I've given so far morphisms were just twisted function types but now
we need morphisms between type constructors or even more restricted
ones morphisms between applicative functions with extra properties
so category theory prescribes this in a general definition of category
can be given which I'm not going to give right now because I don't
see in the use for it other than to indicate the property of natural
T as being similar to previous properties I encourage you to look
at category theory at some point but I will only talk about what I
see it as being useful and so right now it is useful to think about
this as a lifting and the wall is of course need to hold such as identity
and Composition so if we map F to F then we don't change anything
that should be lifted into identity and composition F to G to H mapped
it to composition of those mappings and so on so those are the rigorous
four forms for the naturality war with respect to applicative function
I'm not writing it down in detail because just as naturality with
respect to ordinary type parameter this is this morality with respectively
funter is going to be satisfied automatically by any code that nearly
uses peer and zip and why is that it\textsf{'}s because when we perform a natural
transformation that maps FPR to GD P R and F zip to gzip the code
doesn't actually change at all the code has f as a type parameter
and it just uses pure and zip in the code to cause them as we have
been doing when we implemented the traverse instances for example
so let\textsf{'}s see here is for example we are using zip the zip is from
the function f but F is a type parameter so if we now apply a natural
transformation from F to G for some other negative function G this
code doesn't change at all it still uses the zip and we have the condition
that there\textsf{'}s natural transformation that maps F to G it Maps zip to
zip and peer to peer and and map to map of course that\textsf{'}s the natural
T of natural transformation so our code won't change and our code
therefore is invariant under this natural transformation and so it\textsf{'}s
automatically going to satisfy naturality with respect to the type
parameter F and it also will automatically satisfy not reality with
respect to time over a and that\textsf{'}s why we never need to check these
laws explicitly or even spend so much time writing them explicitly
because they are they are useful sometimes when your reason about
code and prove some other law was then learned are useful but for
coding for implementing you always have natural T automatically so
this concludes chapter 9 and here are some exercises for you to implement
let me just comment and this exercise so I don't want you to prove
laws by hand for this factor T it\textsf{'}s cumbersome but instead use constructions
so we have proved general constructions so if you express T as a recursive
equation using some by factor s and you show that the wife on dress
is by traversable again using constructions of course then you don't
need to and to do the proof yourself if the constructions already
proved once you have found them and similarly for for this construction
you don't need to prove anything by hand this exercise is a little
different but you can try to prove this extra construction that I
mentioned this one but it\textsf{'}s very similar to other constructions and
so it\textsf{'}s not necessarily part of this exercise this concludes chapter
9 
\end{comment}

